Monoid action by iterates of a map #
In this file we define IterateMulAct f
, f : α → α
, as a one field structure wrapper over ℕ
that acts on α
by iterates of f
, ⟨n⟩ • x = f^[n] x
.
It is useful to convert between definitions and theorems about maps and monoid actions.
A structure with a single field val : ℕ
that additively acts on α
by ⟨n⟩ +ᵥ x = f^[n] x
.
- val : ℕ
The value of
n : IterateAddAct f
.
Instances For
A structure with a single field val : ℕ
that acts on α
by ⟨n⟩ • x = f^[n] x
.
- val : ℕ
The value of
n : IterateMulAct f
.
Instances For
theorem
IterateAddAct.ext
{α : Type u_1}
{f : α → α}
{x y : IterateAddAct f}
(val : x.val = y.val)
:
x = y
theorem
IterateMulAct.ext
{α : Type u_1}
{f : α → α}
{x y : IterateMulAct f}
(val : x.val = y.val)
:
x = y
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- IterateMulAct.instCommMonoid = CommMonoid.mk ⋯
Equations
- IterateAddAct.instAddCommMonoid = AddCommMonoid.mk ⋯
Equations
- IterateMulAct.instMulAction = MulAction.mk ⋯ ⋯
Equations
- IterateAddAct.instAddAction = AddAction.mk ⋯ ⋯