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.

structure IterateAddAct {α : Type u_1} (f : α → α) : Type

A structure with a single field val : ℕ that additively acts on α by ⟨n⟩ +ᵥ x = f^[n] x.

• val : ℕ

  The value of n : IterateAddAct f.

theorem IterateMulAct.ext_iff {α : Type u_1} {f : α → α} {x : IterateMulAct f} {y : IterateMulAct f} : x = y ↔ x.val = y.val

theorem IterateAddAct.ext {α : Type u_1} {f : α → α} {x : IterateAddAct f} {y : IterateAddAct f} (val : x.val = y.val) : x = y

theorem IterateAddAct.ext_iff {α : Type u_1} {f : α → α} {x : IterateAddAct f} {y : IterateAddAct f} : x = y ↔ x.val = y.val

theorem IterateMulAct.ext {α : Type u_1} {f : α → α} {x : IterateMulAct f} {y : IterateMulAct f} (val : x.val = y.val) : x = y

structure IterateMulAct {α : Type u_1} (f : α → α) : Type

A structure with a single field val : ℕ that acts on α by ⟨n⟩ • x = f^[n] x.

• val : ℕ

  The value of n : IterateMulAct f.

instance IterateAddAct.instCountable {α : Type u_1} {f : α → α} : Countable (IterateAddAct f)

Equations

• ⋯ = ⋯

instance IterateMulAct.instCountable {α : Type u_1} {f : α → α} : Countable (IterateMulAct f)

Equations

• ⋯ = ⋯

instance IterateAddAct.instAddCommMonoid {α : Type u_1} {f : α → α} : AddCommMonoid (IterateAddAct f)

Equations

• IterateAddAct.instAddCommMonoid = AddCommMonoid.mk ⋯

instance IterateMulAct.instCommMonoid {α : Type u_1} {f : α → α} : CommMonoid (IterateMulAct f)

Equations

• IterateMulAct.instCommMonoid = CommMonoid.mk ⋯

instance IterateAddAct.instAddAction {α : Type u_1} {f : α → α} : AddAction (IterateAddAct f) α

Equations

• IterateAddAct.instAddAction = AddAction.mk ⋯ ⋯

instance IterateMulAct.instMulAction {α : Type u_1} {f : α → α} : MulAction (IterateMulAct f) α

Equations

• IterateMulAct.instMulAction = MulAction.mk ⋯ ⋯

@[simp]

theorem IterateAddAct.mk_vadd {α : Type u_1} {f : α → α} (n : ℕ) (x : α) : { val := n } +ᵥ x = f^[n] x

@[simp]

theorem IterateMulAct.mk_smul {α : Type u_1} {f : α → α} (n : ℕ) (x : α) : { val := n } • x = f^[n] x