equal
deleted
inserted
replaced
62 lemma power3_eq_cube: "a ^ 3 = a * a * a" |
62 lemma power3_eq_cube: "a ^ 3 = a * a * a" |
63 by (simp add: numeral_3_eq_3 mult_assoc) |
63 by (simp add: numeral_3_eq_3 mult_assoc) |
64 |
64 |
65 lemma power_even_eq: |
65 lemma power_even_eq: |
66 "a ^ (2*n) = (a ^ n) ^ 2" |
66 "a ^ (2*n) = (a ^ n) ^ 2" |
67 by (subst OrderedGroup.mult_commute) (simp add: power_mult) |
67 by (subst mult_commute) (simp add: power_mult) |
68 |
68 |
69 lemma power_odd_eq: |
69 lemma power_odd_eq: |
70 "a ^ Suc (2*n) = a * (a ^ n) ^ 2" |
70 "a ^ Suc (2*n) = a * (a ^ n) ^ 2" |
71 by (simp add: power_even_eq) |
71 by (simp add: power_even_eq) |
72 |
72 |