refactor(algebra/group): move monoid.has_pow etc to `algebra.group.…

…defs` (#10147)

This way we can state theorems about `pow`/`nsmul` using notation `^` and `•` right away.

Also move some `ext` lemmas to a new file and rewrite proofs using properties of `monoid_hom`s.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/subalgebra.lean

@@ -107,7 +107,7 @@ S.to_subsemiring.nsmul_mem hx n
 
 theorem zsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) : ∀ (n : ℤ), n • x ∈ S
-| (n : ℕ) := by { rw [zsmul_coe_nat], exact S.nsmul_mem hx n }
+| (n : ℕ) := by { rw [coe_nat_zsmul], exact S.nsmul_mem hx n }
 | -[1+ n] := by { rw [zsmul_neg_succ_of_nat], exact S.neg_mem (S.nsmul_mem hx _) }
 
 theorem coe_nat_mem (n : ℕ) : (n : A) ∈ S :=

src/algebra/big_operators/basic.lean

@@ -1225,6 +1225,11 @@ variables [comm_group β]
 lemma prod_inv_distrib : (∏ x in s, (f x)⁻¹) = (∏ x in s, f x)⁻¹ :=
 (monoid_hom.map_prod (comm_group.inv_monoid_hom : β →* β) f s).symm
 
+@[to_additive zsmul_sum]
+lemma prod_zpow (f : α → β) (s : finset α) (n : ℤ) :
+  (∏ a in s, f a) ^ n = ∏ a in s, (f a) ^ n :=
+(zpow_group_hom n : β →* β).map_prod f s
+
 end comm_group
 
 @[simp] theorem card_sigma {σ : α → Type*} (s : finset α) (t : Π a, finset (σ a)) :
@@ -1257,10 +1262,6 @@ theorem card_eq_sum_card_image [decidable_eq β] (f : α → β) (s : finset α)
   s.card = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :=
 card_eq_sum_card_fiberwise (λ _, mem_image_of_mem _)
 
-lemma zsmul_sum (α β : Type) [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
-  zsmul z (∑ a in s, f a) = ∑ a in s, zsmul z (f a) :=
-add_monoid_hom.map_sum (zsmul_add_group_hom z : β →+ β) f s
-
 @[simp] lemma sum_sub_distrib [add_comm_group β] :
   ∑ x in s, (f x - g x) = (∑ x in s, f x) - (∑ x in s, g x) :=
 by simpa only [sub_eq_add_neg] using sum_add_distrib.trans (congr_arg _ sum_neg_distrib)

src/algebra/group/commute.lean

@@ -90,32 +90,49 @@ end mul_one_class
 
 section monoid
 
-variables {M : Type*} [monoid M]
+variables {M : Type*} [monoid M] {a b : M} {u u₁ u₂ : units M}
 
-@[to_additive] theorem units_inv_right {a : M} {u : units M} : commute a u → commute a ↑u⁻¹ :=
+@[simp, to_additive]
+theorem pow_right (h : commute a b) (n : ℕ) : commute a (b ^ n) := h.pow_right n
+@[simp, to_additive]
+theorem pow_left (h : commute a b) (n : ℕ) : commute (a ^ n) b := (h.symm.pow_right n).symm
+@[simp, to_additive]
+theorem pow_pow (h : commute a b) (m n : ℕ) : commute (a ^ m) (b ^ n) :=
+(h.pow_left m).pow_right n
+
+@[simp, to_additive]
+theorem self_pow (a : M) (n : ℕ) : commute a (a ^ n) := (commute.refl a).pow_right n
+@[simp, to_additive]
+theorem pow_self (a : M) (n : ℕ) : commute (a ^ n) a := (commute.refl a).pow_left n
+@[simp, to_additive]
+theorem pow_pow_self (a : M) (m n : ℕ) : commute (a ^ m) (a ^ n) :=
+(commute.refl a).pow_pow m n
+
+@[to_additive succ_nsmul'] theorem _root_.pow_succ' (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a :=
+(pow_succ a n).trans (self_pow _ _)
+
+@[to_additive] theorem units_inv_right : commute a u → commute a ↑u⁻¹ :=
 semiconj_by.units_inv_right
 
-@[simp, to_additive] theorem units_inv_right_iff {a : M} {u : units M} :
+@[simp, to_additive] theorem units_inv_right_iff :
   commute a ↑u⁻¹ ↔ commute a u :=
 semiconj_by.units_inv_right_iff
 
-@[to_additive] theorem units_inv_left {u : units M} {a : M} : commute ↑u a → commute ↑u⁻¹ a :=
+@[to_additive] theorem units_inv_left : commute ↑u a → commute ↑u⁻¹ a :=
 semiconj_by.units_inv_symm_left
 
 @[simp, to_additive]
-theorem units_inv_left_iff {u : units M} {a : M}: commute ↑u⁻¹ a ↔ commute ↑u a :=
+theorem units_inv_left_iff: commute ↑u⁻¹ a ↔ commute ↑u a :=
 semiconj_by.units_inv_symm_left_iff
 
-variables {u₁ u₂ : units M}
-
 @[to_additive]
 theorem units_coe : commute u₁ u₂ → commute (u₁ : M) u₂ := semiconj_by.units_coe
 @[to_additive]
 theorem units_of_coe : commute (u₁ : M) u₂ → commute u₁ u₂ := semiconj_by.units_of_coe
 @[simp, to_additive]
 theorem units_coe_iff : commute (u₁ : M) u₂ ↔ commute u₁ u₂ := semiconj_by.units_coe_iff
 
-@[to_additive] lemma is_unit_mul_iff {a b : M} (h : commute a b) :
+@[to_additive] lemma is_unit_mul_iff (h : commute a b) :
   is_unit (a * b) ↔ is_unit a ∧ is_unit b :=
 begin
   refine ⟨_, λ H, H.1.mul H.2⟩,
@@ -131,7 +148,7 @@ begin
     rw [mul_assoc, ← hu, u.inv_mul] }
 end
 
-@[simp, to_additive] lemma _root_.is_unit_mul_self_iff {a : M} :
+@[simp, to_additive] lemma _root_.is_unit_mul_self_iff :
   is_unit (a * a) ↔ is_unit a :=
 (commute.refl a).is_unit_mul_iff.trans (and_self _)