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]
@[simp]
theorem
mul_left_iterate
{M : Type u_1}
[monoid M]
(a : M)
(n : ℕ) :
has_mul.mul a^[n] = has_mul.mul (a ^ n)
@[simp]
theorem
add_left_iterate
{M : Type u_1}
[add_monoid M]
(a : M)
(n : ℕ) :
has_add.add a^[n] = has_add.add (n •ℕ a)
@[simp]