# mathlibdocumentation

algebra.iterate_hom

# 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 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.

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

@[simp]
theorem monoid_hom.iterate_map_one {M : Type u_1} [monoid M] (f : M →* M) (n : ) :
f^[n] 1 = 1

@[simp]
theorem add_monoid_hom.iterate_map_zero {M : Type u_1} [add_monoid M] (f : M →+ M) (n : ) :
f^[n] 0 = 0

@[simp]
theorem add_monoid_hom.iterate_map_add {M : Type u_1} [add_monoid M] (f : M →+ M) (n : ) (x y : M) :
f^[n] (x + y) = f^[n] x + f^[n] y

@[simp]
theorem monoid_hom.iterate_map_mul {M : Type u_1} [monoid M] (f : M →* M) (n : ) (x y : M) :
f^[n] (x * y) = (f^[n] x) * f^[n] y

@[simp]
theorem add_monoid_hom.iterate_map_neg {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (x : G) :
f^[n] (-x) = -f^[n] x

@[simp]
theorem monoid_hom.iterate_map_inv {G : Type u_3} [group G] (f : G →* G) (n : ) (x : G) :

theorem monoid_hom.iterate_map_pow {M : Type u_1} [monoid M] (f : M →* M) (a : M) (n m : ) :
f^[n] (a ^ m) = f^[n] a ^ m

theorem monoid_hom.iterate_map_gpow {G : Type u_3} [group G] (f : G →* G) (a : G) (n : ) (m : ) :
f^[n] (a ^ m) = f^[n] a ^ m

@[simp]
theorem add_monoid_hom.iterate_map_sub {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (x y : G) :
f^[n] (x - y) = f^[n] x - f^[n] y

theorem add_monoid_hom.iterate_map_smul {M : Type u_1} [add_monoid M] (f : M →+ M) (n m : ) (x : M) :
f^[n] (m •ℕ x) = m •ℕ f^[n] x

theorem add_monoid_hom.iterate_map_gsmul {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (m : ) (x : G) :
f^[n] (m •ℤ x) = m •ℤ f^[n] x

theorem ring_hom.coe_pow {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
(f ^ n) = (f^[n])

theorem ring_hom.iterate_map_one {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
f^[n] 1 = 1

theorem ring_hom.iterate_map_zero {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
f^[n] 0 = 0

theorem ring_hom.iterate_map_add {R : Type u_5} [semiring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x + y) = f^[n] x + f^[n] y

theorem ring_hom.iterate_map_mul {R : Type u_5} [semiring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x * y) = (f^[n] x) * f^[n] y

theorem ring_hom.iterate_map_pow {R : Type u_5} [semiring R] (f : R →+* R) (a : R) (n m : ) :
f^[n] (a ^ m) = f^[n] a ^ m

theorem ring_hom.iterate_map_smul {R : Type u_5} [semiring R] (f : R →+* R) (n m : ) (x : R) :
f^[n] (m •ℕ x) = m •ℕ f^[n] x

theorem ring_hom.iterate_map_sub {R : Type u_5} [ring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x - y) = f^[n] x - f^[n] y

theorem ring_hom.iterate_map_neg {R : Type u_5} [ring R] (f : R →+* R) (n : ) (x : R) :
f^[n] (-x) = -f^[n] x

theorem ring_hom.iterate_map_gsmul {R : Type u_5} [ring R] (f : R →+* R) (n : ) (m : ) (x : R) :
f^[n] (m •ℤ x) = m •ℤ f^[n] x

@[simp]
theorem mul_left_iterate {M : Type u_1} [monoid M] (a : M) (n : ) :
= has_mul.mul (a ^ n)

@[simp]
theorem add_left_iterate {M : Type u_1} [add_monoid M] (a : M) (n : ) :

@[simp]
theorem mul_right_iterate {M : Type u_1} [monoid M] (a : M) (n : ) :
(λ (x : M), x * a)^[n] = λ (x : M), x * a ^ n

@[simp]
theorem add_right_iterate {M : Type u_1} [add_monoid M] (a : M) (n : ) :
(λ (x : M), x + a)^[n] = λ (x : M), x + n •ℕ a