Documentation

Mathlib.GroupTheory.GroupAction.IterateAct

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 : αα) :

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

Instances For
    structure IterateMulAct {α : Type u_1} (f : αα) :

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

    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
      instance IterateMulAct.instCountable {α : Type u_1} {f : αα} :
      Equations
      • =
      instance IterateAddAct.instCountable {α : Type u_1} {f : αα} :
      Equations
      • =
      instance IterateMulAct.instCommMonoid {α : Type u_1} {f : αα} :
      Equations
      instance IterateAddAct.instAddCommMonoid {α : Type u_1} {f : αα} :
      Equations
      instance IterateMulAct.instMulAction {α : Type u_1} {f : αα} :
      Equations
      instance IterateAddAct.instAddAction {α : Type u_1} {f : αα} :
      Equations
      @[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