equal
deleted
inserted
replaced
70 poly_minus :: "'a list => 'a list" ("-- _" [80] 80) where |
70 poly_minus :: "'a list => 'a list" ("-- _" [80] 80) where |
71 "-- p = (- 1) %* p" |
71 "-- p = (- 1) %* p" |
72 |
72 |
73 definition (in semiring_0) |
73 definition (in semiring_0) |
74 divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where |
74 divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where |
75 [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))" |
75 [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))" |
76 |
76 |
77 --{*order of a polynomial*} |
77 --{*order of a polynomial*} |
78 definition (in ring_1) order :: "'a => 'a list => nat" where |
78 definition (in ring_1) order :: "'a => 'a list => nat" where |
79 "order a p = (SOME n. ([-a, 1] %^ n) divides p & |
79 "order a p = (SOME n. ([-a, 1] %^ n) divides p & |
80 ~ (([-a, 1] %^ (Suc n)) divides p))" |
80 ~ (([-a, 1] %^ (Suc n)) divides p))" |