HepLean 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.

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

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

Instances For
    source
    theorem IterateMulAct.ext_iff {α : Type u_1} {f : α → α} {x : IterateMulAct f} {y : IterateMulAct f} :
    x = y ↔ x.val = y.val
    source
    theorem IterateAddAct.ext {α : Type u_1} {f : α → α} {x : IterateAddAct f} {y : IterateAddAct f} (val : x.val = y.val) :
    x = y
    source
    theorem IterateAddAct.ext_iff {α : Type u_1} {f : α → α} {x : IterateAddAct f} {y : IterateAddAct f} :
    x = y ↔ x.val = y.val
    source
    theorem IterateMulAct.ext {α : Type u_1} {f : α → α} {x : IterateMulAct f} {y : IterateMulAct f} (val : x.val = y.val) :
    x = y
    source
    structure IterateMulAct {α : Type u_1} (f : α → α) :
    Type

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

    Instances For
      source
      instance IterateAddAct.instCountable {α : Type u_1} {f : α → α} :
      Countable (IterateAddAct f)
      Equations
      • ⋯ = ⋯
      source
      instance IterateMulAct.instCountable {α : Type u_1} {f : α → α} :
      Countable (IterateMulAct f)
      Equations
      • ⋯ = ⋯
      source
      theorem IterateAddAct.instAddCommMonoid.proof_4 {α : Type u_1} {f : α → α} :
      ∀ (x : IterateAddAct f), (fun (n : ℕ) (a : IterateAddAct f) => { val := n * a.val }) 0 x = 0
      source
      theorem IterateAddAct.instAddCommMonoid.proof_6 {α : Type u_1} {f : α → α} :
      ∀ (x x_1 : IterateAddAct f), x + x_1 = x_1 + x
      source
      theorem IterateAddAct.instAddCommMonoid.proof_1 {α : Type u_1} {f : α → α} (a : IterateAddAct f) (b : IterateAddAct f) (c : IterateAddAct f) :
      a + b + c = a + (b + c)
      source
      theorem IterateAddAct.instAddCommMonoid.proof_3 {α : Type u_1} {f : α → α} :
      ∀ (x : IterateAddAct f), x + 0 = x + 0
      source
      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
      source
      theorem IterateAddAct.instAddCommMonoid.proof_2 {α : Type u_1} {f : α → α} :
      ∀ (x : IterateAddAct f), 0 + x = x
      source
      instance IterateAddAct.instAddCommMonoid {α : Type u_1} {f : α → α} :
      AddCommMonoid (IterateAddAct f)
      Equations
      source
      instance IterateMulAct.instCommMonoid {α : Type u_1} {f : α → α} :
      CommMonoid (IterateMulAct f)
      Equations
      source
      instance IterateAddAct.instAddAction {α : Type u_1} {f : α → α} :
      AddAction (IterateAddAct f) α
      Equations
      source
      theorem IterateAddAct.instAddAction.proof_1 {α : Type u_1} {f : α → α} :
      ∀ (x : α), 0 +ᵥ x = 0 +ᵥ x
      source
      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)
      source
      instance IterateMulAct.instMulAction {α : Type u_1} {f : α → α} :
      MulAction (IterateMulAct f) α
      Equations
      source
      @[simp]
      theorem IterateAddAct.mk_vadd {α : Type u_1} {f : α → α} (n : ℕ) (x : α) :
      { val := n } +ᵥ x = f^[n] x
      source
      @[simp]
      theorem IterateMulAct.mk_smul {α : Type u_1} {f : α → α} (n : ℕ) (x : α) :
      { val := n } • x = f^[n] x