| changeset 11093 | 62c2e0af1d30 |
| parent 7998 | 3d0c34795831 |
| child 13735 | 7de9342aca7a |
| 11092:69c1abb9a129 | 11093:62c2e0af1d30 |
|---|---|
10 lcoeff :: "'a::ringS up => 'a" |
10 lcoeff :: "'a::ringS up => 'a" |
11 eucl_size :: 'a::ringS => nat |
11 eucl_size :: 'a::ringS => nat |
12 |
12 |
13 defs |
13 defs |
14 lcoeff_def "lcoeff p == coeff (deg p) p" |
14 lcoeff_def "lcoeff p == coeff (deg p) p" |
15 eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1" |
15 eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1" |
16 |
16 |
17 end |
17 end |
18 |
18 |