Documentation

Mathlib.Algebra.Group.PowIterate

Powers on monoid of functions #

If F is a type of functions from α onto itself equipped with a monoid structure such that 1 is the identity and multiplication is given by composition, then natural exponentiation corresponds to iteration of composition.

This is separated from the Mathlib.Algebra.Group.IsApply file to avoid importing Monoid there.

source
class IsNPowApplyEqIterate (F : Type u_1) {α : outParam (Type u_2)} [FunLike F α α] [NPow F] :
Prop

IsNPowApplyEqIterate F states for all x : α, (f ^ n) x = f^[n] x.

  • pow_apply_eq_iterate (f : F) (n : ℕ) (x : α) : (f ^ n) x = (⇑f)^[n] x
Instances
    source
    theorem pow_apply_eq_iterate {F : Type u_1} {α : outParam (Type u_2)} {inst✝ : FunLike F α α} {inst✝¹ : NPow F} [self : IsNPowApplyEqIterate F] (f : F) (n : ℕ) (x : α) :
    (f ^ n) x = (⇑f)^[n] x

    Alias of IsNPowApplyEqIterate.pow_apply_eq_iterate.

    source
    instance instIsNPowApplyEqIterateOfIsOneApplyEqSelfOfIsMulApplyEqComp {F : Type u_1} {α : Type u_2} [FunLike F α α] [Monoid F] [IsOneApplyEqSelf F] [IsMulApplyEqComp F] :
    IsNPowApplyEqIterate F
    source
    theorem FunLike.coe_pow_eq_iterate {F : Type u_1} {α : Type u_2} [FunLike F α α] [NPow F] [IsNPowApplyEqIterate F] (f : F) (n : ℕ) :
    ⇑(f ^ n) = (⇑f)^[n]