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]
@[simp]
theorem
mul_left_iterate
{G : Type u_3}
[monoid G]
(a : G)
(n : ℕ) :
has_mul.mul a^[n] = has_mul.mul (a ^ n)
theorem
semiconj_by.function_semiconj_mul_left
{G : Type u_3}
[semigroup G]
{a b c : G}
(h : semiconj_by a b c) :
function.semiconj (has_mul.mul a) (has_mul.mul b) (has_mul.mul c)
theorem
add_semiconj_by.function_semiconj_add_left
{G : Type u_3}
[add_semigroup G]
{a b c : G}
(h : add_semiconj_by a b c) :
function.semiconj (has_add.add a) (has_add.add b) (has_add.add c)
theorem
commute.function_commute_mul_left
{G : Type u_3}
[semigroup G]
{a b : G}
(h : commute a b) :
function.commute (has_mul.mul a) (has_mul.mul b)
theorem
add_commute.function_commute_add_left
{G : Type u_3}
[add_semigroup G]
{a b : G}
(h : add_commute a b) :
function.commute (has_add.add a) (has_add.add b)
theorem
add_semiconj_by.function_semiconj_add_right_swap
{G : Type u_3}
[add_semigroup G]
{a b c : G}
(h : add_semiconj_by a b c) :
function.semiconj (λ (_x : G), _x + a) (λ (_x : G), _x + c) (λ (_x : G), _x + b)
theorem
semiconj_by.function_semiconj_mul_right_swap
{G : Type u_3}
[semigroup G]
{a b c : G}
(h : semiconj_by a b c) :
function.semiconj (λ (_x : G), _x * a) (λ (_x : G), _x * c) (λ (_x : G), _x * b)
theorem
add_commute.function_commute_add_right
{G : Type u_3}
[add_semigroup G]
{a b : G}
(h : add_commute a b) :
function.commute (λ (_x : G), _x + a) (λ (_x : G), _x + b)
theorem
commute.function_commute_mul_right
{G : Type u_3}
[semigroup G]
{a b : G}
(h : commute a b) :
function.commute (λ (_x : G), _x * a) (λ (_x : G), _x * b)
@[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]