equal
deleted
inserted
replaced
375 qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd) |
375 qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd) |
376 |
376 |
377 |
377 |
378 end |
378 end |
379 |
379 |
380 context normalization_semidom |
380 context normalization_semidom_multiplicative |
381 begin |
381 begin |
382 |
382 |
383 lemma normalize_power: "normalize (a ^ n) = normalize a ^ n" |
383 lemma normalize_power: "normalize (a ^ n) = normalize a ^ n" |
384 by (induct n) (simp_all add: normalize_mult) |
384 by (induct n) (simp_all add: normalize_mult) |
385 |
385 |