Theorems · Theorem · dynamical systems

MulAction.zpow_smul_mod_minimalPeriod

∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (a : G) (b : α) (n : ℤ),
  a ^ (n % ↑(Function.minimalPeriod (fun x => a • x) b)) • b = a ^ n • b

Defined in

Mathlib.Dynamics.PeriodicPts.Defs

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulAction