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)
:
theorem
IterateMulAct.ext
{α : Type u_1}
{f : α → α}
{x y : IterateMulAct f}
(val : x.val = y.val)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- IterateMulAct.instMulAction = { smul := fun (n : IterateMulAct f) (x : α) => f^[n.val] x, one_smul := ⋯, mul_smul := ⋯ }
Equations
- IterateAddAct.instAddAction = { vadd := fun (n : IterateAddAct f) (x : α) => f^[n.val] x, zero_vadd := ⋯, add_vadd := ⋯ }