chore(algebra/iterate_hom): use to_additive to fill missing lemmas (#…

…10886)

src/algebra/iterate_hom.lean

@@ -14,7 +14,7 @@ import group_theory.perm.basic
 Iterate of a monoid/ring homomorphism is a monoid/ring homomorphism but it has a wrong type, so Lean
 can't apply lemmas like `monoid_hom.map_one` to `f^[n] 1`. Though it is possible to define
 a monoid structure on the endomorphisms, quite often we do not want to convert from
-`M →* M` to (not yet defined) `monoid.End M` and from `f^[n]` to `f^n` just to apply a simple lemma.
+`M →* M` to `monoid.End M` and from `f^[n]` to `f^n` just to apply a simple lemma.
 
 So, we restate standard `*_hom.map_*` lemmas under names `*_hom.iterate_map_*`.
 
@@ -59,36 +59,46 @@ theorem iterate_map_inv (f : G →* G) (n : ℕ) (x) :
   f^[n] (x⁻¹) = (f^[n] x)⁻¹ :=
 commute.iterate_left f.map_inv n x
 
-theorem iterate_map_pow (f : M →* M) (a) (n m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
+@[simp, to_additive]
+theorem iterate_map_div (f : G →* G) (n : ℕ) (x y) :
+  f^[n] (x / y) = (f^[n] x) / (f^[n] y) :=
+semiconj₂.iterate f.map_div n x y
+
+theorem iterate_map_pow (f : M →* M) (n : ℕ) (a) (m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
 commute.iterate_left (λ x, f.map_pow x m) n a
 
-theorem iterate_map_zpow (f : G →* G) (a) (n : ℕ) (m : ℤ) : f^[n] (a^m) = (f^[n] a)^m :=
+theorem iterate_map_zpow (f : G →* G) (n : ℕ) (a) (m : ℤ) : f^[n] (a^m) = (f^[n] a)^m :=
 commute.iterate_left (λ x, f.map_zpow x m) n a
 
 lemma coe_pow {M} [comm_monoid M] (f : monoid.End M) (n : ℕ) : ⇑(f^n) = (f^[n]) :=
 hom_coe_pow _ rfl (λ f g, rfl) _ _
 
 end monoid_hom
 
-namespace add_monoid_hom
-
-variables [add_monoid M] [add_monoid N] [add_group G] [add_group H]
+lemma monoid.End.coe_pow {M} [monoid M] (f : monoid.End M) (n : ℕ) : ⇑(f^n) = (f^[n]) :=
+hom_coe_pow _ rfl (λ f g, rfl) _ _
 
-@[simp]
-theorem iterate_map_sub (f : G →+ G) (n : ℕ) (x y) :
-  f^[n] (x - y) = (f^[n] x) - (f^[n] y) :=
-semiconj₂.iterate f.map_sub n x y
+-- we define these manually so that we can pick a better argument order
+namespace add_monoid_hom
+variables [add_monoid M] [add_group G]
 
 theorem iterate_map_smul (f : M →+ M) (n m : ℕ) (x : M) :
   f^[n] (m • x) = m • (f^[n] x) :=
-f.to_multiplicative.iterate_map_pow x n m
+f.to_multiplicative.iterate_map_pow n x m
+
+attribute [to_additive iterate_map_smul, to_additive_reorder 5] monoid_hom.iterate_map_pow
 
 theorem iterate_map_zsmul (f : G →+ G) (n : ℕ) (m : ℤ) (x : G) :
   f^[n] (m • x) = m • (f^[n] x) :=
-f.to_multiplicative.iterate_map_zpow x n m
+f.to_multiplicative.iterate_map_zpow n x m
+
+attribute [to_additive, to_additive_reorder 5] monoid_hom.iterate_map_zpow
 
 end add_monoid_hom
 
+lemma add_monoid.End.coe_pow {A} [add_monoid A] (f : add_monoid.End A) (n : ℕ) : ⇑(f^n) = (f^[n]) :=
+hom_coe_pow _ rfl (λ f g, rfl) _ _
+
 namespace ring_hom
 
 section semiring
@@ -109,7 +119,7 @@ theorem iterate_map_mul : f^[n] (x * y) = (f^[n] x) * (f^[n] y) :=
 f.to_monoid_hom.iterate_map_mul n x y
 
 theorem iterate_map_pow (a) (n m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
-f.to_monoid_hom.iterate_map_pow a n m
+f.to_monoid_hom.iterate_map_pow n a m
 
 theorem iterate_map_smul (n m : ℕ) (x : R) :
   f^[n] (m • x) = m • (f^[n] x) :=