src/HOL/Nat_Numeral.thy
changeset 44345 881c324470a2
parent 43531 cc46a678faaf
child 44766 d4d33a4d7548
equal deleted inserted replaced
44344:49be3e7d4762 44345:881c324470a2
   124   unfolding power2_eq_square by simp
   124   unfolding power2_eq_square by simp
   125 
   125 
   126 lemma power2_eq_1_iff:
   126 lemma power2_eq_1_iff:
   127   "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   127   "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   128   unfolding power2_eq_square by (rule square_eq_1_iff)
   128   unfolding power2_eq_square by (rule square_eq_1_iff)
       
   129 
       
   130 end
       
   131 
       
   132 context idom
       
   133 begin
       
   134 
       
   135 lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
       
   136   unfolding power2_eq_square by (rule square_eq_iff)
   129 
   137 
   130 end
   138 end
   131 
   139 
   132 context linordered_ring
   140 context linordered_ring
   133 begin
   141 begin