equal
deleted
inserted
replaced
45 lemma "(4::int) + 0 = 4" |
45 lemma "(4::int) + 0 = 4" |
46 apply algebra? |
46 apply algebra? |
47 by simp |
47 by simp |
48 |
48 |
49 lemma |
49 lemma |
50 assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0" |
50 assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0" |
51 shows "d^2*c^2 - 2*d*c*a*f + a^2*f^2 - e*d*b*c - e*b*a*f + a*e^2*c + f*d*b^2 = 0" |
51 shows "d\<^sup>2*c\<^sup>2 - 2*d*c*a*f + a\<^sup>2 * f\<^sup>2 - e*d*b*c - e*b*a*f + a*e\<^sup>2*c + f*d*b\<^sup>2 = 0" |
52 using assms by algebra |
52 using assms by algebra |
53 |
53 |
54 lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)" |
54 lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)" |
55 by algebra |
55 by algebra |
56 |
56 |
57 theorem "x* (x\<^sup>2 - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
57 theorem "x* (x\<^sup>2 - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
58 by algebra |
58 by algebra |
59 |
59 |
60 lemma |
60 lemma |
61 fixes x::"'a::{idom}" |
61 fixes x::"'a::idom" |
62 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
62 shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = 1 & y = 1 | x = 0 & y = 0" |
63 by algebra |
63 by algebra |
64 |
64 |
65 subsection {* Lemmas for Lagrange's theorem *} |
65 subsection {* Lemmas for Lagrange's theorem *} |
66 |
66 |
67 definition |
67 definition |