equal
deleted
inserted
replaced
44 by algebra |
44 by algebra |
45 |
45 |
46 theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
46 theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
47 by algebra |
47 by algebra |
48 |
48 |
|
49 lemma fixes x::"'a::{idom,recpower,number_ring}" |
|
50 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
|
51 by algebra |
49 |
52 |
50 subsection {* Lemmas for Lagrange's theorem *} |
53 subsection {* Lemmas for Lagrange's theorem *} |
51 |
54 |
52 definition |
55 definition |
53 sq :: "'a::times => 'a" where |
56 sq :: "'a::times => 'a" where |