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.

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.

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

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• IterateMulAct.instMulAction = { smul := fun (n : IterateMulAct f) (x : α) => f^[n.val] x, one_smul := ⋯, mul_smul := ⋯ }

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

Equations

• IterateAddAct.instAddAction = { vadd := fun (n : IterateAddAct f) (x : α) => f^[n.val] x, zero_vadd := ⋯, add_vadd := ⋯ }

@[simp]

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

@[simp]

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