src/HOL/Power.thy
changeset 60685 cb21b7022b00
parent 60155 91477b3a2d6b
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Power.thy	Wed Jul 08 00:04:15 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Jul 08 14:01:34 2015 +0200
     1.3 @@ -306,6 +306,19 @@
     1.4  
     1.5  end
     1.6  
     1.7 +context normalization_semidom
     1.8 +begin
     1.9 +
    1.10 +lemma normalize_power:
    1.11 +  "normalize (a ^ n) = normalize a ^ n"
    1.12 +  by (induct n) (simp_all add: normalize_mult)
    1.13 +
    1.14 +lemma unit_factor_power:
    1.15 +  "unit_factor (a ^ n) = unit_factor a ^ n"
    1.16 +  by (induct n) (simp_all add: unit_factor_mult)
    1.17 +
    1.18 +end
    1.19 +
    1.20  context division_ring
    1.21  begin
    1.22