author | huffman |
Wed, 14 Jan 2009 13:47:14 -0800 | |
changeset 29485 | ec072307c69b |
parent 29481 | 3e8420c1124a |
child 29486 | 23a26d17adc0 |
child 29492 | b19b8793b71c |
child 29530 | 9905b660612b |
--- a/src/HOL/Fundamental_Theorem_Algebra.thy Wed Jan 14 19:38:55 2009 +0100 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy Wed Jan 14 13:47:14 2009 -0800 @@ -970,6 +970,7 @@ definition order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat" where + [code del]: "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)" lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"