Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module algebra.hom.iterate
! leanprover-community/mathlib commit 792a2a264169d64986541c6f8f7e3bbb6acb6295
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.GroupTheory.GroupAction.Opposite

/-!
# Iterates of monoid and ring homomorphisms

Iterate of a monoid/ring homomorphism is a monoid/ring homomorphism but it has a wrong type, so Lean
can't apply lemmas like `MonoidHom.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 `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_*`.

We also prove formulas for iterates of add/mul left/right.

## Tags

homomorphism, iterate
-/

open Function

variable {M: Type ?u.46544M : Type _: Type (?u.2+1)Type _} {N: Type ?u.17N : Type _: Type (?u.17+1)Type _} {G: Type ?u.34788G : Type _: Type (?u.8+1)Type _} {H: Type ?u.32619H : Type _: Type (?u.51637+1)Type _}

/-- An auxiliary lemma that can be used to prove `β(f ^ n) = (βf^[n])`. -/
theorem hom_coe_pow: β {F : Type u_1} [inst : Monoid F] (c : F β M β M),
c 1 = id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow {F: Type ?u.26F : Type _: Type (?u.26+1)Type _} [Monoid: Type ?u.29 β Type ?u.29Monoid F: Type ?u.26F] (c: F β M β Mc : F: Type ?u.26F β M: Type ?u.14M β M: Type ?u.14M) (h1: c 1 = idh1 : c: F β M β Mc 1: ?m.401 = id: {Ξ± : Sort ?u.370} β Ξ± β Ξ±id)
(hmul: β (f g : F), c (f * g) = c f β c ghmul : β f: ?m.413f g: ?m.416g, c: F β M β Mc (f: ?m.413f * g: ?m.416g) = c: F β M β Mc f: ?m.413f β c: F β M β Mc g: ?m.416g) (f: Ff : F: Type ?u.26F) : β n: ?m.1010n, c: F β M β Mc (f: Ff ^ n: ?m.1010n) = c: F β M β Mc f: Ff^[n: ?m.1010n]
| 0: β0 => byGoals accomplished! π
M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fc (f ^ 0) = c f^[0]rw [M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fc (f ^ 0) = c f^[0]pow_zero: β {M : Type ?u.1287} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fc 1 = c f^[0] M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fc (f ^ 0) = c f^[0]h1: c 1 = idh1M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fid = c f^[0]]M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fid = c f^[0]
M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fc (f ^ 0) = c f^[0]rflGoals accomplished! π
| n: βn + 1 => byGoals accomplished! π M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f ^ (n + 1)) = c f^[n + 1]rw [M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f ^ (n + 1)) = c f^[n + 1]pow_succ: β {M : Type ?u.1382} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_succ,M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f * f ^ n) = c f^[n + 1] M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f ^ (n + 1)) = c f^[n + 1]iterate_succ': β {Ξ± : Type ?u.1426} (f : Ξ± β Ξ±) (n : β), f^[Nat.succ n] = f β f^[n]iterate_succ',M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f * f ^ n) = c f β c f^[n] M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f ^ (n + 1)) = c f^[n + 1]hmul: β (f g : F), c (f * g) = c f β c ghmul,M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc f β c (f ^ n) = c f β c f^[n] M: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc (f ^ (n + 1)) = c f^[n + 1]hom_coe_pow: β {F : Type u_1} [inst : Monoid F] (c : F β M β M),
c 1 = id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow c: F β M β Mc h1: c 1 = idh1 hmul: β (f g : F), c (f * g) = c f β c ghmul f: Ff n: βnM: Type u_2N: Type ?u.17G: Type ?u.20H: Type ?u.23F: Type u_1instβ: Monoid Fc: F β M β Mh1: c 1 = idhmul: β (f g : F), c (f * g) = c f β c gf: Fn: βc f β c f^[n] = c f β c f^[n]]Goals accomplished! π
#align hom_coe_pow hom_coe_pow: β {M : Type u_2} {F : Type u_1} [inst : Monoid F] (c : F β M β M),
c 1 = id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow

namespace MonoidHom

section

variable [MulOneClass: Type ?u.2631 β Type ?u.2631MulOneClass M: Type ?u.1575M] [MulOneClass: Type ?u.1590 β Type ?u.1590MulOneClass N: Type ?u.1578N]

@[to_additive: β {M : Type u_1} [inst : AddZeroClass M] (f : M β+ M) (n : β), (βf^[n]) 0 = 0to_additive (attr := simp)]
theorem iterate_map_one: β {M : Type u_1} [inst : MulOneClass M] (f : M β* M) (n : β), (βf^[n]) 1 = 1iterate_map_one (f: M β* Mf : M: Type ?u.1593M β* M: Type ?u.1593M) (n: βn : β: Typeβ) : (f: M β* Mf^[n: βn]) 1: ?m.20201 = 1: ?m.24821 :=
iterate_fixed: β {Ξ± : Type ?u.2501} {f : Ξ± β Ξ±} {x : Ξ±}, f x = x β β (n : β), (f^[n]) x = xiterate_fixed f: M β* Mf.map_one: β {M : Type ?u.2505} {N : Type ?u.2506} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M β* N), βf 1 = 1map_one n: βn
#align monoid_hom.iterate_map_one MonoidHom.iterate_map_one: β {M : Type u_1} [inst : MulOneClass M] (f : M β* M) (n : β), (βf^[n]) 1 = 1MonoidHom.iterate_map_one
#align add_monoid_hom.iterate_map_zero AddMonoidHom.iterate_map_zero: β {M : Type u_1} [inst : AddZeroClass M] (f : M β+ M) (n : β), (βf^[n]) 0 = 0AddMonoidHom.iterate_map_zero

@[to_additive: β {M : Type u_1} [inst : AddZeroClass M] (f : M β+ M) (n : β) (x y : M), (βf^[n]) (x + y) = (βf^[n]) x + (βf^[n]) yto_additive (attr := simp)]
theorem iterate_map_mul: β (f : M β* M) (n : β) (x y : M), (βf^[n]) (x * y) = (βf^[n]) x * (βf^[n]) yiterate_map_mul (f: M β* Mf : M: Type ?u.2619M β* M: Type ?u.2619M) (n: βn : β: Typeβ) (x: Mx y: My) : (f: M β* Mf^[n: βn]) (x: ?m.2650x * y: ?m.2653y) = (f: M β* Mf^[n: βn]) x: ?m.2650x * (f: M β* Mf^[n: βn]) y: ?m.2653y :=
Semiconjβ.iterate: β {Ξ± : Type ?u.4657} {f : Ξ± β Ξ±} {op : Ξ± β Ξ± β Ξ±}, Semiconjβ f op op β β (n : β), Semiconjβ (f^[n]) op opSemiconjβ.iterate f: M β* Mf.map_mul: β {M : Type ?u.4661} {N : Type ?u.4662} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M β* N) (a b : M),
βf (a * b) = βf a * βf bmap_mul n: βn x: Mx y: My
#align monoid_hom.iterate_map_mul MonoidHom.iterate_map_mul: β {M : Type u_1} [inst : MulOneClass M] (f : M β* M) (n : β) (x y : M), (βf^[n]) (x * y) = (βf^[n]) x * (βf^[n]) yMonoidHom.iterate_map_mul

end

variable [Monoid: Type ?u.7992 β Type ?u.7992Monoid M: Type ?u.4835M] [Monoid: Type ?u.6192 β Type ?u.6192Monoid N: Type ?u.4838N] [Group: Type ?u.4829 β Type ?u.4829Group G: Type ?u.4841G] [Group: Type ?u.4832 β Type ?u.4832Group H: Type ?u.7989H]

@[to_additive: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (x : G), (βf^[n]) (-x) = -(βf^[n]) xto_additive (attr := simp)]
theorem iterate_map_inv: β (f : G β* G) (n : β) (x : G), (βf^[n]) xβ»ΒΉ = ((βf^[n]) x)β»ΒΉiterate_map_inv (f: G β* Gf : G: Type ?u.4841G β* G: Type ?u.4841G) (n: βn : β: Typeβ) (x: Gx) : (f: G β* Gf^[n: βn]) x: ?m.5113xβ»ΒΉ = ((f: G β* Gf^[n: βn]) x: ?m.5113x)β»ΒΉ :=
Commute.iterate_left: β {Ξ± : Type ?u.6001} {f g : Ξ± β Ξ±}, Function.Commute f g β β (n : β), Function.Commute (f^[n]) gCommute.iterate_left f: G β* Gf.map_inv: β {Ξ± : Type ?u.6005} {Ξ² : Type ?u.6006} [inst : Group Ξ±] [inst_1 : DivisionMonoid Ξ²] (f : Ξ± β* Ξ²) (a : Ξ±),
βf aβ»ΒΉ = (βf a)β»ΒΉmap_inv n: βn x: Gx
#align monoid_hom.iterate_map_inv MonoidHom.iterate_map_inv: β {G : Type u_1} [inst : Group G] (f : G β* G) (n : β) (x : G), (βf^[n]) xβ»ΒΉ = ((βf^[n]) x)β»ΒΉMonoidHom.iterate_map_inv
#align add_monoid_hom.iterate_map_neg AddMonoidHom.iterate_map_neg: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (x : G), (βf^[n]) (-x) = -(βf^[n]) xAddMonoidHom.iterate_map_neg

@[to_additive: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (x y : G), (βf^[n]) (x - y) = (βf^[n]) x - (βf^[n]) yto_additive (attr := simp)]
theorem iterate_map_div: β (f : G β* G) (n : β) (x y : G), (βf^[n]) (x / y) = (βf^[n]) x / (βf^[n]) yiterate_map_div (f: G β* Gf : G: Type ?u.6183G β* G: Type ?u.6183G) (n: βn : β: Typeβ) (x: Gx y: Gy) : (f: G β* Gf^[n: βn]) (x: ?m.6455x / y: ?m.6458y) = (f: G β* Gf^[n: βn]) x: ?m.6455x / (f: G β* Gf^[n: βn]) y: ?m.6458y :=
Semiconjβ.iterate: β {Ξ± : Type ?u.7779} {f : Ξ± β Ξ±} {op : Ξ± β Ξ± β Ξ±}, Semiconjβ f op op β β (n : β), Semiconjβ (f^[n]) op opSemiconjβ.iterate f: G β* Gf.map_div: β {Ξ± : Type ?u.7783} {Ξ² : Type ?u.7784} [inst : Group Ξ±] [inst_1 : DivisionMonoid Ξ²] (f : Ξ± β* Ξ²) (g h : Ξ±),
βf (g / h) = βf g / βf hmap_div n: βn x: Gx y: Gy
#align monoid_hom.iterate_map_div MonoidHom.iterate_map_div: β {G : Type u_1} [inst : Group G] (f : G β* G) (n : β) (x y : G), (βf^[n]) (x / y) = (βf^[n]) x / (βf^[n]) yMonoidHom.iterate_map_div
#align add_monoid_hom.iterate_map_sub AddMonoidHom.iterate_map_sub: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (x y : G), (βf^[n]) (x - y) = (βf^[n]) x - (βf^[n]) yAddMonoidHom.iterate_map_sub

theorem iterate_map_pow: β (f : M β* M) (n : β) (a : M) (m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_pow (f: M β* Mf : M: Type ?u.7980M β* M: Type ?u.7980M) (n: βn : β: Typeβ) (a: Ma) (m: βm : β: Typeβ) : (f: M β* Mf^[n: βn]) (a: ?m.8241a ^ m: βm) = (f: M β* Mf^[n: βn]) a: ?m.8241a ^ m: βm :=
Commute.iterate_left: β {Ξ± : Type ?u.14012} {f g : Ξ± β Ξ±}, Function.Commute f g β β (n : β), Function.Commute (f^[n]) gCommute.iterate_left (fun x: ?m.14017x => f: M β* Mf.map_pow: β {M : Type ?u.14019} {N : Type ?u.14020} [inst : Monoid M] [inst_1 : Monoid N] (f : M β* N) (a : M) (n : β),
βf (a ^ n) = βf a ^ nmap_pow x: ?m.14017x m: βm) n: βn a: Ma
#align monoid_hom.iterate_map_pow MonoidHom.iterate_map_pow: β {M : Type u_1} [inst : Monoid M] (f : M β* M) (n : β) (a : M) (m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ mMonoidHom.iterate_map_pow

theorem iterate_map_zpow: β (f : G β* G) (n : β) (a : G) (m : β€), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_zpow (f: G β* Gf : G: Type ?u.14072G β* G: Type ?u.14072G) (n: βn : β: Typeβ) (a: ?m.14344a) (m: β€m : β€: Typeβ€) : (f: G β* Gf^[n: βn]) (a: ?m.14344a ^ m: β€m) = (f: G β* Gf^[n: βn]) a: ?m.14344a ^ m: β€m :=
Commute.iterate_left: β {Ξ± : Type ?u.20274} {f g : Ξ± β Ξ±}, Function.Commute f g β β (n : β), Function.Commute (f^[n]) gCommute.iterate_left (fun x: ?m.20279x => f: G β* Gf.map_zpow: β {Ξ± : Type ?u.20281} {Ξ² : Type ?u.20282} [inst : Group Ξ±] [inst_1 : DivisionMonoid Ξ²] (f : Ξ± β* Ξ²) (g : Ξ±) (n : β€),
βf (g ^ n) = βf g ^ nmap_zpow x: ?m.20279x m: β€m) n: βn a: Ga
#align monoid_hom.iterate_map_zpow MonoidHom.iterate_map_zpow: β {G : Type u_1} [inst : Group G] (f : G β* G) (n : β) (a : G) (m : β€), (βf^[n]) (a ^ m) = (βf^[n]) a ^ mMonoidHom.iterate_map_zpow

theorem coe_pow: β {M : Type u_1} [inst : CommMonoid M] (f : Monoid.End M) (n : β), β(f ^ n) = βf^[n]coe_pow {M: Type u_1M} [CommMonoid: Type ?u.20403 β Type ?u.20403CommMonoid M: ?m.20400M] (f: Monoid.End Mf : Monoid.End: (M : Type ?u.20406) β [inst : MulOneClass M] β Type ?u.20406Monoid.End M: ?m.20400M) (n: βn : β: Typeβ) : β(f: Monoid.End Mf ^ n: βn) = f: Monoid.End Mf^[n: βn] :=
hom_coe_pow: β {M : Type ?u.25127} {F : Type ?u.25126} [inst : Monoid F] (c : F β M β M),
c 1 = _root_.id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow _: ?m.25129 β ?m.25128 β ?m.25128_ rfl: β {Ξ± : Sort ?u.25132} {a : Ξ±}, a = arfl (fun _: ?m.25542_ _: ?m.25545_ => rfl: β {Ξ± : Sort ?u.25547} {a : Ξ±}, a = arfl) _: ?m.25129_ _: β_
#align monoid_hom.coe_pow MonoidHom.coe_pow: β {M : Type u_1} [inst : CommMonoid M] (f : Monoid.End M) (n : β), β(f ^ n) = βf^[n]MonoidHom.coe_pow

end MonoidHom

theorem Monoid.End.coe_pow: β {M : Type u_1} [inst : Monoid M] (f : Monoid.End M) (n : β), β(f ^ n) = βf^[n]Monoid.End.coe_pow {M: ?m.25658M} [Monoid: Type ?u.25661 β Type ?u.25661Monoid M: ?m.25658M] (f: Monoid.End Mf : Monoid.End: (M : Type ?u.25664) β [inst : MulOneClass M] β Type ?u.25664Monoid.End M: ?m.25658M) (n: βn : β: Typeβ) : β(f: Monoid.End Mf ^ n: βn) = f: Monoid.End Mf^[n: βn] :=
hom_coe_pow: β {M : Type ?u.30268} {F : Type ?u.30267} [inst : Monoid F] (c : F β M β M),
c 1 = id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow _: ?m.30270 β ?m.30269 β ?m.30269_ rfl: β {Ξ± : Sort ?u.30273} {a : Ξ±}, a = arfl (fun _: ?m.30683_ _: ?m.30686_ => rfl: β {Ξ± : Sort ?u.30688} {a : Ξ±}, a = arfl) _: ?m.30270_ _: β_
#align monoid.End.coe_pow Monoid.End.coe_pow: β {M : Type u_1} [inst : Monoid M] (f : Monoid.End M) (n : β), β(f ^ n) = βf^[n]Monoid.End.coe_pow

-- we define these manually so that we can pick a better argument order

theorem iterate_map_smul: β (f : M β+ M) (n m : β) (x : M), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_smul (f: M β+ Mf : M: Type ?u.30805M β+ M: Type ?u.30805M) (n: βn m: βm : β: Typeβ) (x: Mx : M: Type ?u.30805M) : (f: M β+ Mf^[n: βn]) (m: βm β’ x: Mx) = m: βm β’ (f: M β+ Mf^[n: βn]) x: Mx :=
f: M β+ Mf.toMultiplicative: {Ξ± : Type ?u.32368} β
{Ξ² : Type ?u.32367} β
[inst : AddZeroClass Ξ±] β [inst_1 : AddZeroClass Ξ²] β (Ξ± β+ Ξ²) β (Multiplicative Ξ± β* Multiplicative Ξ²)toMultiplicative.iterate_map_pow: β {M : Type ?u.32501} [inst : Monoid M] (f : M β* M) (n : β) (a : M) (m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_pow n: βn x: Mx m: βm
#align add_monoid_hom.iterate_map_smul AddMonoidHom.iterate_map_smul: β {M : Type u_1} [inst : AddMonoid M] (f : M β+ M) (n m : β) (x : M), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xAddMonoidHom.iterate_map_smul

attribute [to_additive: β {M : Type u_1} [inst : AddMonoid M] (f : M β+ M) (n m : β) (a : M), (βf^[n]) (m β’ a) = m β’ (βf^[n]) ato_additive (reorder := 5 6)] MonoidHom.iterate_map_pow: β {M : Type u_1} [inst : Monoid M] (f : M β* M) (n : β) (a : M) (m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ mMonoidHom.iterate_map_pow
#align add_monoid_hom.iterate_map_nsmul AddMonoidHom.iterate_map_nsmul: β {M : Type u_1} [inst : AddMonoid M] (f : M β+ M) (n m : β) (a : M), (βf^[n]) (m β’ a) = m β’ (βf^[n]) aAddMonoidHom.iterate_map_nsmul

theorem iterate_map_zsmul: β (f : G β+ G) (n : β) (m : β€) (x : G), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_zsmul (f: G β+ Gf : G: Type ?u.32616G β+ G: Type ?u.32616G) (n: βn : β: Typeβ) (m: β€m : β€: Typeβ€) (x: Gx : G: Type ?u.32616G) : (f: G β+ Gf^[n: βn]) (m: β€m β’ x: Gx) = m: β€m β’ (f: G β+ Gf^[n: βn]) x: Gx :=
f: G β+ Gf.toMultiplicative: {Ξ± : Type ?u.34381} β
{Ξ² : Type ?u.34380} β
[inst : AddZeroClass Ξ±] β [inst_1 : AddZeroClass Ξ²] β (Ξ± β+ Ξ²) β (Multiplicative Ξ± β* Multiplicative Ξ²)toMultiplicative.iterate_map_zpow: β {G : Type ?u.34712} [inst : Group G] (f : G β* G) (n : β) (a : G) (m : β€), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_zpow n: βn x: Gx m: β€m
#align add_monoid_hom.iterate_map_zsmul AddMonoidHom.iterate_map_zsmul: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (m : β€) (x : G), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xAddMonoidHom.iterate_map_zsmul

attribute [to_additive: β {G : Type u_1} [inst : AddGroup G] (f : G β+ G) (n : β) (m : β€) (x : G), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xto_additive existing (reorder := 5 6)] MonoidHom.iterate_map_zpow: β {G : Type u_1} [inst : Group G] (f : G β* G) (n : β) (a : G) (m : β€), (βf^[n]) (a ^ m) = (βf^[n]) a ^ mMonoidHom.iterate_map_zpow

hom_coe_pow: β {M : Type ?u.39873} {F : Type ?u.39872} [inst : Monoid F] (c : F β M β M),
c 1 = id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow _: ?m.39875 β ?m.39874 β ?m.39874_ rfl: β {Ξ± : Sort ?u.39878} {a : Ξ±}, a = arfl (fun _: ?m.40288_ _: ?m.40291_ => rfl: β {Ξ± : Sort ?u.40293} {a : Ξ±}, a = arfl) _: ?m.39875_ _: β_

namespace RingHom

section Semiring

variable {R: Type ?u.45356R : Type _: Type (?u.40406+1)Type _} [Semiring: Type ?u.40409 β Type ?u.40409Semiring R: Type ?u.40451R] (f: R β+* Rf : R: Type ?u.40406R β+* R: Type ?u.45356R) (n: βn : β: Typeβ) (x: Rx y: Ry : R: Type ?u.40406R)

theorem coe_pow: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β), β(f ^ n) = βf^[n]coe_pow (n: βn : β: Typeβ) : β(f: R β+* Rf ^ n: βn) = f: R β+* Rf^[n: βn] :=
hom_coe_pow: β {M : Type ?u.44849} {F : Type ?u.44848} [inst : Monoid F] (c : F β M β M),
c 1 = _root_.id β (β (f g : F), c (f * g) = c f β c g) β β (f : F) (n : β), c (f ^ n) = c f^[n]hom_coe_pow _: ?m.44851 β ?m.44850 β ?m.44850_ rfl: β {Ξ± : Sort ?u.44854} {a : Ξ±}, a = arfl (fun _: ?m.45264_ _: ?m.45267_ => rfl: β {Ξ± : Sort ?u.45269} {a : Ξ±}, a = arfl) f: R β+* Rf n: βn
#align ring_hom.coe_pow RingHom.coe_pow: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β), β(f ^ n) = βf^[n]RingHom.coe_pow

theorem iterate_map_one: (βf^[n]) 1 = 1iterate_map_one : (f: R β+* Rf^[n: βn]) 1: ?m.457281 = 1: ?m.457651 :=
f: R β+* Rf.toMonoidHom: {Ξ± : Type ?u.45783} β
{Ξ² : Type ?u.45782} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β* Ξ²toMonoidHom.iterate_map_one: β {M : Type ?u.45807} [inst : MulOneClass M] (f : M β* M) (n : β), (βf^[n]) 1 = 1iterate_map_one n: βn
#align ring_hom.iterate_map_one RingHom.iterate_map_one: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β), (βf^[n]) 1 = 1RingHom.iterate_map_one

theorem iterate_map_zero: (βf^[n]) 0 = 0iterate_map_zero : (f: R β+* Rf^[n: βn]) 0: ?m.462370 = 0: ?m.463690 :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.46387} β
{Ξ² : Type ?u.46386} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_zero: β {M : Type ?u.46411} [inst : AddZeroClass M] (f : M β+ M) (n : β), (βf^[n]) 0 = 0iterate_map_zero n: βn
#align ring_hom.iterate_map_zero RingHom.iterate_map_zero: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β), (βf^[n]) 0 = 0RingHom.iterate_map_zero

theorem iterate_map_add: (βf^[n]) (x + y) = (βf^[n]) x + (βf^[n]) yiterate_map_add : (f: R β+* Rf^[n: βn]) (x: Rx + y: Ry) = (f: R β+* Rf^[n: βn]) x: Rx + (f: R β+* Rf^[n: βn]) y: Ry :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.47887} β
{Ξ² : Type ?u.47886} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_add: β {M : Type ?u.47911} [inst : AddZeroClass M] (f : M β+ M) (n : β) (x y : M), (βf^[n]) (x + y) = (βf^[n]) x + (βf^[n]) yiterate_map_add n: βn x: Rx y: Ry
#align ring_hom.iterate_map_add RingHom.iterate_map_add: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β) (x y : R), (βf^[n]) (x + y) = (βf^[n]) x + (βf^[n]) yRingHom.iterate_map_add

theorem iterate_map_mul: (βf^[n]) (x * y) = (βf^[n]) x * (βf^[n]) yiterate_map_mul : (f: R β+* Rf^[n: βn]) (x: Rx * y: Ry) = (f: R β+* Rf^[n: βn]) x: Rx * (f: R β+* Rf^[n: βn]) y: Ry :=
f: R β+* Rf.toMonoidHom: {Ξ± : Type ?u.49407} β
{Ξ² : Type ?u.49406} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β* Ξ²toMonoidHom.iterate_map_mul: β {M : Type ?u.49431} [inst : MulOneClass M] (f : M β* M) (n : β) (x y : M), (βf^[n]) (x * y) = (βf^[n]) x * (βf^[n]) yiterate_map_mul n: βn x: Rx y: Ry
#align ring_hom.iterate_map_mul RingHom.iterate_map_mul: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n : β) (x y : R), (βf^[n]) (x * y) = (βf^[n]) x * (βf^[n]) yRingHom.iterate_map_mul

theorem iterate_map_pow: β (a : R) (n m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_pow (a: ?m.49530a) (n: βn m: βm : β: Typeβ) : (f: R β+* Rf^[n: βn]) (a: ?m.49530a ^ m: βm) = (f: R β+* Rf^[n: βn]) a: ?m.49530a ^ m: βm :=
f: R β+* Rf.toMonoidHom: {Ξ± : Type ?u.50418} β
{Ξ² : Type ?u.50417} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β* Ξ²toMonoidHom.iterate_map_pow: β {M : Type ?u.50442} [inst : Monoid M] (f : M β* M) (n : β) (a : M) (m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ miterate_map_pow n: βn a: Ra m: βm
#align ring_hom.iterate_map_pow RingHom.iterate_map_pow: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (a : R) (n m : β), (βf^[n]) (a ^ m) = (βf^[n]) a ^ mRingHom.iterate_map_pow

theorem iterate_map_smul: β (n m : β) (x : R), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_smul (n: βn m: βm : β: Typeβ) (x: Rx : R: Type ?u.50517R) : (f: R β+* Rf^[n: βn]) (m: βm β’ x: Rx) = m: βm β’ (f: R β+* Rf^[n: βn]) x: Rx :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.51468} β
{Ξ² : Type ?u.51467} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_smul: β {M : Type ?u.51492} [inst : AddMonoid M] (f : M β+ M) (n m : β) (x : M), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_smul n: βn m: βm x: Rx
#align ring_hom.iterate_map_smul RingHom.iterate_map_smul: β {R : Type u_1} [inst : Semiring R] (f : R β+* R) (n m : β) (x : R), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xRingHom.iterate_map_smul

end Semiring

variable {R: Type ?u.51640R : Type _: Type (?u.53234+1)Type _} [Ring: Type ?u.53237 β Type ?u.53237Ring R: Type ?u.51805R] (f: R β+* Rf : R: Type ?u.51640R β+* R: Type ?u.51640R) (n: βn : β: Typeβ) (x: Rx y: Ry : R: Type ?u.51640R)

theorem iterate_map_sub: (βf^[n]) (x - y) = (βf^[n]) x - (βf^[n]) yiterate_map_sub : (f: R β+* Rf^[n: βn]) (x: Rx - y: Ry) = (f: R β+* Rf^[n: βn]) x: Rx - (f: R β+* Rf^[n: βn]) y: Ry :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.53029} β
{Ξ² : Type ?u.53028} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_sub: β {G : Type ?u.53173} [inst : AddGroup G] (f : G β+ G) (n : β) (x y : G), (βf^[n]) (x - y) = (βf^[n]) x - (βf^[n]) yiterate_map_sub n: βn x: Rx y: Ry
#align ring_hom.iterate_map_sub RingHom.iterate_map_sub: β {R : Type u_1} [inst : Ring R] (f : R β+* R) (n : β) (x y : R), (βf^[n]) (x - y) = (βf^[n]) x - (βf^[n]) yRingHom.iterate_map_sub

theorem iterate_map_neg: β {R : Type u_1} [inst : Ring R] (f : R β+* R) (n : β) (x : R), (βf^[n]) (-x) = -(βf^[n]) xiterate_map_neg : (f: R β+* Rf^[n: βn]) (-x: Rx) = -(f: R β+* Rf^[n: βn]) x: Rx :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.54072} β
{Ξ² : Type ?u.54071} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_neg: β {G : Type ?u.54216} [inst : AddGroup G] (f : G β+ G) (n : β) (x : G), (βf^[n]) (-x) = -(βf^[n]) xiterate_map_neg n: βn x: Rx
#align ring_hom.iterate_map_neg RingHom.iterate_map_neg: β {R : Type u_1} [inst : Ring R] (f : R β+* R) (n : β) (x : R), (βf^[n]) (-x) = -(βf^[n]) xRingHom.iterate_map_neg

theorem iterate_map_zsmul: β (n : β) (m : β€) (x : R), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_zsmul (n: βn : β: Typeβ) (m: β€m : β€: Typeβ€) (x: Rx : R: Type ?u.54273R) : (f: R β+* Rf^[n: βn]) (m: β€m β’ x: Rx) = m: β€m β’ (f: R β+* Rf^[n: βn]) x: Rx :=
f: R β+* Rf.toAddMonoidHom: {Ξ± : Type ?u.55207} β
{Ξ² : Type ?u.55206} β [inst : NonAssocSemiring Ξ±] β [inst_1 : NonAssocSemiring Ξ²] β (Ξ± β+* Ξ²) β Ξ± β+ Ξ²toAddMonoidHom.iterate_map_zsmul: β {G : Type ?u.55351} [inst : AddGroup G] (f : G β+ G) (n : β) (m : β€) (x : G), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xiterate_map_zsmul n: βn m: β€m x: Rx
#align ring_hom.iterate_map_zsmul RingHom.iterate_map_zsmul: β {R : Type u_1} [inst : Ring R] (f : R β+* R) (n : β) (m : β€) (x : R), (βf^[n]) (m β’ x) = m β’ (βf^[n]) xRingHom.iterate_map_zsmul

end RingHom

--what should be the namespace for this section?
section Monoid

variable [Monoid: Type ?u.59884 β Type ?u.59884Monoid G: Type ?u.55404G] (a: Ga : G: Type ?u.55423G) (n: βn : β: Typeβ)

@[to_additive: β {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] (a : G) (n : β) [inst_1 : AddAction G H],
(fun x => a +α΅₯ x)^[n] = fun x => n β’ a +α΅₯ xto_additive (attr := simp)]
theorem smul_iterate: β [inst : MulAction G H], (fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate [MulAction: (Ξ± : Type ?u.55437) β Type ?u.55436 β [inst : Monoid Ξ±] β Type (max?u.55437?u.55436)MulAction G: Type ?u.55423G H: Type ?u.55426H] : (a: Ga β’ Β· : H: Type ?u.55426H β H: Type ?u.55426H)^[n: βn] = (a: Ga ^ n: βn β’ Β·) :=
funext: β {Ξ± : Sort ?u.59360} {Ξ² : Ξ± β Sort ?u.59359} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun b: ?m.59375b =>
Nat.recOn: β {motive : β β Sort ?u.59377} (t : β), motive Nat.zero β (β (n : β), motive n β motive (Nat.succ n)) β motive tNat.recOn n: βn (byGoals accomplished! π M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: H((fun x => a β’ x)^[Nat.zero]) b = a ^ Nat.zero β’ brw [M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: H((fun x => a β’ x)^[Nat.zero]) b = a ^ Nat.zero β’ biterate_zero: β {Ξ± : Type ?u.59415} (f : Ξ± β Ξ±), f^[0] = iditerate_zero,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: Hid b = a ^ Nat.zero β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: H((fun x => a β’ x)^[Nat.zero]) b = a ^ Nat.zero β’ bid.def: β {Ξ± : Sort ?u.59432} (a : Ξ±), id a = aid.def,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: Hb = a ^ Nat.zero β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: H((fun x => a β’ x)^[Nat.zero]) b = a ^ Nat.zero β’ bpow_zero: β {M : Type ?u.59441} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: Hb = 1 β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: H((fun x => a β’ x)^[Nat.zero]) b = a ^ Nat.zero β’ bone_smul: β (M : Type ?u.59501) {Ξ± : Type ?u.59500} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β’ b = bone_smulM: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gn: βinstβ: MulAction G Hb: Hb = b]Goals accomplished! π)
fun n: ?m.59406n ih: ?m.59409ih => byGoals accomplished! π M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ brw [M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ biterate_succ': β {Ξ± : Type ?u.59539} (f : Ξ± β Ξ±) (n : β), f^[Nat.succ n] = f β f^[n]iterate_succ',M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x) β (fun x => a β’ x)^[n]) b = a ^ Nat.succ n β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ bcomp_apply: β {Ξ² : Sort ?u.59553} {Ξ΄ : Sort ?u.59554} {Ξ± : Sort ?u.59555} {f : Ξ² β Ξ΄} {g : Ξ± β Ξ²} {x : Ξ±}, (f β g) x = f (g x)comp_apply,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ ba β’ ((fun x => a β’ x)^[n]) b = a ^ Nat.succ n β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ bih: ((fun x => a β’ x)^[n]) b = a ^ n β’ bih,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ ba β’ a ^ n β’ b = a ^ Nat.succ n β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ bpow_succ: β {M : Type ?u.59580} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_succ,M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ ba β’ a ^ n β’ b = (a * a ^ n) β’ b M: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ b((fun x => a β’ x)^[Nat.succ n]) b = a ^ Nat.succ n β’ bmul_smul: β {Ξ± : Type ?u.59636} {Ξ² : Type ?u.59635} [inst : Monoid Ξ±] [self : MulAction Ξ± Ξ²] (x y : Ξ±) (b : Ξ²),
(x * y) β’ b = x β’ y β’ bmul_smulM: Type ?u.55417N: Type ?u.55420G: Type u_1H: Type u_2instβΒΉ: Monoid Ga: Gnβ: βinstβ: MulAction G Hb: Hn: βih: ((fun x => a β’ x)^[n]) b = a ^ n β’ ba β’ a ^ n β’ b = a β’ a ^ n β’ b]Goals accomplished! π
#align smul_iterate smul_iterate: β {G : Type u_1} {H : Type u_2} [inst : Monoid G] (a : G) (n : β) [inst_1 : MulAction G H],
(fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate
#align vadd_iterate vadd_iterate: β {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] (a : G) (n : β) [inst_1 : AddAction G H],
(fun x => a +α΅₯ x)^[n] = fun x => n β’ a +α΅₯ xvadd_iterate

@[to_additive: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), (fun x => a + x)^[n] = fun x => n β’ a + xto_additive (attr := simp)]
theorem mul_left_iterate: (fun x => a * x)^[n] = fun x => a ^ n * xmul_left_iterate : (a: Ga * Β·)^[n: βn] = (a: Ga ^ n: βn * Β·) :=
smul_iterate: β {G : Type ?u.63109} {H : Type ?u.63110} [inst : Monoid G] (a : G) (n : β) [inst_1 : MulAction G H],
(fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate a: Ga n: βn
#align mul_left_iterate mul_left_iterate: β {G : Type u_1} [inst : Monoid G] (a : G) (n : β), (fun x => a * x)^[n] = fun x => a ^ n * xmul_left_iterate
#align add_left_iterate add_left_iterate: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), (fun x => a + x)^[n] = fun x => n β’ a + xadd_left_iterate

@[to_additive: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), (fun x => x + a)^[n] = fun x => x + n β’ ato_additive (attr := simp)]
theorem mul_right_iterate: (fun x => x * a)^[n] = fun x => x * a ^ nmul_right_iterate : (Β· * a: Ga)^[n: βn] = (Β· * a: Ga ^ n: βn) :=
smul_iterate: β {G : Type ?u.67134} {H : Type ?u.67135} [inst : Monoid G] (a : G) (n : β) [inst_1 : MulAction G H],
(fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate (MulOpposite.op: {Ξ± : Type ?u.67139} β Ξ± β Ξ±α΅α΅α΅MulOpposite.op a: Ga) n: βn
#align mul_right_iterate mul_right_iterate: β {G : Type u_1} [inst : Monoid G] (a : G) (n : β), (fun x => x * a)^[n] = fun x => x * a ^ nmul_right_iterate
#align add_right_iterate add_right_iterate: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), (fun x => x + a)^[n] = fun x => x + n β’ aadd_right_iterate

@[to_additive: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), ((fun x => x + a)^[n]) 0 = n β’ ato_additive]
theorem mul_right_iterate_apply_one: ((fun x => x * a)^[n]) 1 = a ^ nmul_right_iterate_apply_one : ((Β· * a: Ga)^[n: βn]) 1: ?m.678921 = a: Ga ^ n: βn := byGoals accomplished! π M: Type ?u.67258N: Type ?u.67261G: Type u_1H: Type ?u.67267instβ: Monoid Ga: Gn: β((fun x => x * a)^[n]) 1 = a ^ nsimp [mul_right_iterate: β {G : Type ?u.70709} [inst : Monoid G] (a : G) (n : β), (fun x => x * a)^[n] = fun x => x * a ^ nmul_right_iterate]Goals accomplished! π
#align mul_right_iterate_apply_one mul_right_iterate_apply_one: β {G : Type u_1} [inst : Monoid G] (a : G) (n : β), ((fun x => x * a)^[n]) 1 = a ^ nmul_right_iterate_apply_one
#align add_right_iterate_apply_zero add_right_iterate_apply_zero: β {G : Type u_1} [inst : AddMonoid G] (a : G) (n : β), ((fun x => x + a)^[n]) 0 = n β’ aadd_right_iterate_apply_zero

@[to_additive: β {G : Type u_1} [inst : AddMonoid G] (n j : β), (fun x => n β’ x)^[j] = fun x => n ^ j β’ xto_additive (attr := simp)]
theorem pow_iterate: β (n j : β), (fun x => x ^ n)^[j] = fun x => x ^ n ^ jpow_iterate (n: βn : β: Typeβ) (j: βj : β: Typeβ) : (fun x: Gx : G: Type ?u.71290G => x: Gx ^ n: βn)^[j: βj] = fun x: Gx : G: Type ?u.71290G => x: Gx ^ n: βn ^ j: βj :=
letI : MulAction: (Ξ± : Type ?u.76351) β Type ?u.76350 β [inst : Monoid Ξ±] β Type (max?u.76351?u.76350)MulAction β: Typeβ G: Type ?u.71290G :=
{ smul := fun n: ?m.76376n g: ?m.76379g => g: ?m.76379g ^ n: ?m.76376n
one_smul := pow_one: β {M : Type ?u.78906} [inst : Monoid M] (a : M), a ^ 1 = apow_one
mul_smul := fun m: ?m.78952m n: ?m.78955n g: ?m.78958g => pow_mul': β {M : Type ?u.78960} [inst : Monoid M] (a : M) (m n : β), a ^ (m * n) = (a ^ n) ^ mpow_mul' g: ?m.78958g m: ?m.78952m n: ?m.78955n }
smul_iterate: β {G : Type ?u.78970} {H : Type ?u.78971} [inst : Monoid G] (a : G) (n : β) [inst_1 : MulAction G H],
(fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate n: βn j: βj
#align pow_iterate pow_iterate: β {G : Type u_1} [inst : Monoid G] (n j : β), (fun x => x ^ n)^[j] = fun x => x ^ n ^ jpow_iterate
#align nsmul_iterate nsmul_iterate: β {G : Type u_1} [inst : AddMonoid G] (n j : β), (fun x => n β’ x)^[j] = fun x => n ^ j β’ xnsmul_iterate

end Monoid

section Group

variable [Group: Type ?u.79093 β Type ?u.79093Group G: Type ?u.79087G]

@[to_additive: β {G : Type u_1} [inst : AddGroup G] (n : β€) (j : β), (fun x => n β’ x)^[j] = fun x => n ^ j β’ xto_additive (attr := simp)]
theorem zpow_iterate: β (n : β€) (j : β), (fun x => x ^ n)^[j] = fun x => x ^ n ^ jzpow_iterate (n: β€n : β€: Typeβ€) (j: βj : β: Typeβ) : (fun x: Gx : G: Type ?u.79102G => x: Gx ^ n: β€n)^[j: βj] = fun x: ?m.81762x => x: ?m.81762x ^ n: β€n ^ j: βj :=
letI : MulAction: (Ξ± : Type ?u.82077) β Type ?u.82076 β [inst : Monoid Ξ±] β Type (max?u.82077?u.82076)MulAction β€: Typeβ€ G: Type ?u.79102G :=
{ smul := fun n: ?m.82101n g: ?m.82104g => g: ?m.82104g ^ n: ?m.82101n
one_smul := zpow_one: β {G : Type ?u.84696} [inst : DivInvMonoid G] (a : G), a ^ 1 = azpow_one
mul_smul := fun m: ?m.84749m n: ?m.84752n g: ?m.84755g => zpow_mul': β {Ξ± : Type ?u.84757} [inst : DivisionMonoid Ξ±] (a : Ξ±) (m n : β€), a ^ (m * n) = (a ^ n) ^ mzpow_mul' g: ?m.84755g m: ?m.84749m n: ?m.84752n }
smul_iterate: β {G : Type ?u.84806} {H : Type ?u.84807} [inst : Monoid G] (a : G) (n : β) [inst_1 : MulAction G H],
(fun x => a β’ x)^[n] = fun x => a ^ n β’ xsmul_iterate n: β€n j: βj
#align zpow_iterate zpow_iterate: β {G : Type u_1} [inst : Group G] (n : β€) (j : β), (fun x => x ^ n)^[j] = fun x => x ^ n ^ jzpow_iterate
#align zsmul_iterate zsmul_iterate: β {G : Type u_1} [inst : AddGroup G] (n : β€) (j : β), (fun x => n β’ x)^[j] = fun x => n ^ j β’ xzsmul_iterate

end Group

section Semigroup

variable [Semigroup: Type ?u.89663 β Type ?u.89663Semigroup G: Type ?u.87808G] {a: Ga b: Gb c: Gc : G: Type ?u.84944G}

-- Porting note: need `dsimp only`, see https://leanprover.zulipchat.com/#narrow/stream/
-- 287929-mathlib4/topic/dsimp.20before.20rw/near/317063489
@[to_additive: β {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
AddSemiconjBy a b c β Semiconj (fun x => a + x) (fun x => b + x) fun x => c + xto_additive]
theorem SemiconjBy.function_semiconj_mul_left: β {G : Type u_1} [inst : Semigroup G] {a b c : G},
SemiconjBy a b c β Semiconj (fun x => a * x) (fun x => b * x) fun x => c * xSemiconjBy.function_semiconj_mul_left (h: SemiconjBy a b ch : SemiconjBy: {M : Type ?u.84959} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga b: Gb c: Gc) :
Function.Semiconj: {Ξ± : Type ?u.85486} β {Ξ² : Type ?u.85485} β (Ξ± β Ξ²) β (Ξ± β Ξ±) β (Ξ² β Ξ²) β PropFunction.Semiconj (a: Ga * Β·) (b: Gb * Β·) (c: Gc * Β·) := fun j: ?m.87126j => byGoals accomplished! π
M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: G(fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)dsimp onlyM: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * (b * j) = c * (a * j);M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * (b * j) = c * (a * j) M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: G(fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)rw [M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * (b * j) = c * (a * j)β mul_assoc: β {G : Type ?u.87153} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * b * j = c * (a * j) M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * (b * j) = c * (a * j)h: SemiconjBy a b ch.eq: β {S : Type ?u.87196} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Gc * a * j = c * (a * j) M: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Ga * (b * j) = c * (a * j)mul_assoc: β {G : Type ?u.87713} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocM: Type ?u.84938N: Type ?u.84941G: Type u_1H: Type ?u.84947instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Gc * (a * j) = c * (a * j)]Goals accomplished! π
#align semiconj_by.function_semiconj_mul_left SemiconjBy.function_semiconj_mul_left: β {G : Type u_1} [inst : Semigroup G] {a b c : G},
SemiconjBy a b c β Semiconj (fun x => a * x) (fun x => b * x) fun x => c * xSemiconjBy.function_semiconj_mul_left
AddSemiconjBy a b c β Semiconj (fun x => a + x) (fun x => b + x) fun x => c + xAddSemiconjBy.function_semiconj_add_left

@[to_additive: β {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b β Function.Commute (fun x => a + x) fun x => b + xto_additive]
theorem Commute.function_commute_mul_left: β {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b β Function.Commute (fun x => a * x) fun x => b * xCommute.function_commute_mul_left (h: _root_.Commute a bh : _root_.Commute: {S : Type ?u.87823} β [inst : Mul S] β S β S β Prop_root_.Commute a: Ga b: Gb) :
Function.Commute: {Ξ± : Type ?u.88349} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropFunction.Commute (a: Ga * Β·) (b: Gb * Β·) :=
SemiconjBy.function_semiconj_mul_left: β {G : Type ?u.89575} [inst : Semigroup G] {a b c : G},
SemiconjBy a b c β Semiconj (fun x => a * x) (fun x => b * x) fun x => c * xSemiconjBy.function_semiconj_mul_left h: _root_.Commute a bh
#align commute.function_commute_mul_left Commute.function_commute_mul_left: β {G : Type u_1} [inst : Semigroup G] {a b : G}, _root_.Commute a b β Function.Commute (fun x => a * x) fun x => b * xCommute.function_commute_mul_left

@[to_additive: β {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
AddSemiconjBy a b c β Semiconj (fun x => x + a) (fun x => x + c) fun x => x + bto_additive]
theorem SemiconjBy.function_semiconj_mul_right_swap: SemiconjBy a b c β Semiconj (fun x => x * a) (fun x => x * c) fun x => x * bSemiconjBy.function_semiconj_mul_right_swap (h: SemiconjBy a b ch : SemiconjBy: {M : Type ?u.89672} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga b: Gb c: Gc) :
Function.Semiconj: {Ξ± : Type ?u.90199} β {Ξ² : Type ?u.90198} β (Ξ± β Ξ²) β (Ξ± β Ξ±) β (Ξ² β Ξ²) β PropFunction.Semiconj (Β· * a: Ga) (Β· * c: Gc) (Β· * b: Gb) := fun j: ?m.91839j => byGoals accomplished! π M: Type ?u.89651N: Type ?u.89654G: Type u_1H: Type ?u.89660instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: G(fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)simp_rw [M: Type ?u.89651N: Type ?u.89654G: Type u_1H: Type ?u.89660instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Gj * c * a = j * a * bmul_assoc: β {G : Type ?u.91917} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,M: Type ?u.89651N: Type ?u.89654G: Type u_1H: Type ?u.89660instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: Gj * (c * a) = j * (a * b) M: Type ?u.89651N: Type ?u.89654G: Type u_1H: Type ?u.89660instβ: Semigroup Ga, b, c: Gh: SemiconjBy a b cj: G(fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)β h: SemiconjBy a b ch.eq: β {S : Type ?u.91982} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeqGoals accomplished! π]Goals accomplished! π
#align semiconj_by.function_semiconj_mul_right_swap SemiconjBy.function_semiconj_mul_right_swap: β {G : Type u_1} [inst : Semigroup G] {a b c : G},
SemiconjBy a b c β Semiconj (fun x => x * a) (fun x => x * c) fun x => x * bSemiconjBy.function_semiconj_mul_right_swap