| changeset 23331 | da040caa0596 |
| parent 23273 | c6d5ab154c7c |
| child 23338 | 3f1a453cb538 |
--- a/src/HOL/ex/Groebner_Examples.thy Mon Jun 11 18:28:16 2007 +0200 +++ b/src/HOL/ex/Groebner_Examples.thy Mon Jun 11 18:34:12 2007 +0200 @@ -46,6 +46,9 @@ theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" by algebra +lemma fixes x::"'a::{idom,recpower,number_ring}" +shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" +by algebra subsection {* Lemmas for Lagrange's theorem *}