Documentation
Mathlib
.
Algebra
.
Ring
.
Hom
.
IterateHom
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.GroupPower.IterateHom
Mathlib.Algebra.Ring.Hom.Defs
Imported by
RingHom
.
coe_pow
Lemma iterates of ring homomorphisms
#
source
theorem
RingHom
.
coe_pow
{α :
Type
u_1}
[
Semiring
α
]
(f :
α
→+*
α
)
(n :
ℕ
)
:
⇑
(
f
^
n
)
=
(
⇑
f
)
^[
n
]