src/HOL/ex/Groebner_Examples.thy
changeset 23331 da040caa0596
parent 23273 c6d5ab154c7c
child 23338 3f1a453cb538
equal deleted inserted replaced
23330:01c09922ce59 23331:da040caa0596
    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