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

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

    Instances For
      instance IterateAddAct.instCountable {α : Type u_1} {f : αα} :
      Equations
      • =
      instance IterateMulAct.instCountable {α : Type u_1} {f : αα} :
      Equations
      • =
      theorem IterateAddAct.instAddCommMonoid.proof_4 {α : Type u_1} {f : αα} :
      ∀ (x : IterateAddAct f), (fun (n : ) (a : IterateAddAct f) => { val := n * a.val }) 0 x = 0
      theorem IterateAddAct.instAddCommMonoid.proof_6 {α : Type u_1} {f : αα} :
      ∀ (x x_1 : IterateAddAct f), x + x_1 = x_1 + x
      theorem IterateAddAct.instAddCommMonoid.proof_1 {α : Type u_1} {f : αα} (a : IterateAddAct f) (b : IterateAddAct f) (c : IterateAddAct f) :
      a + b + c = a + (b + c)
      theorem IterateAddAct.instAddCommMonoid.proof_3 {α : Type u_1} {f : αα} :
      ∀ (x : IterateAddAct f), x + 0 = x + 0
      theorem IterateAddAct.instAddCommMonoid.proof_5 {α : Type u_1} {f : αα} (n : ) (a : IterateAddAct f) :
      (fun (n : ) (a : IterateAddAct f) => { val := n * a.val }) (n + 1) a = (fun (n : ) (a : IterateAddAct f) => { val := n * a.val }) n a + a
      theorem IterateAddAct.instAddCommMonoid.proof_2 {α : Type u_1} {f : αα} :
      ∀ (x : IterateAddAct f), 0 + x = x
      instance IterateAddAct.instAddCommMonoid {α : Type u_1} {f : αα} :
      Equations
      instance IterateMulAct.instCommMonoid {α : Type u_1} {f : αα} :
      Equations
      instance IterateAddAct.instAddAction {α : Type u_1} {f : αα} :
      Equations
      theorem IterateAddAct.instAddAction.proof_1 {α : Type u_1} {f : αα} :
      ∀ (x : α), 0 +ᵥ x = 0 +ᵥ x
      theorem IterateAddAct.instAddAction.proof_2 {α : Type u_1} {f : αα} :
      ∀ (x x_1 : IterateAddAct f) (x_2 : α), f^[x.val + x_1.val] x_2 = f^[x.val] (f^[x_1.val] x_2)
      instance IterateMulAct.instMulAction {α : Type u_1} {f : αα} :
      Equations
      @[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