English
For a multiplicative action of M on α and a ∈ α, the period of m acting on a is defined as the least positive n with m^n • a = a, or 0 if no such n exists.
Русский
Для мультипликативного действия M на α и элемента a ∈ α период действия m на a определяется как наименьшее положительное n такое, что m^n • a = a, либо 0, если такого n не существует.
LaTeX
$$$ \\text{period}(m,a) = \\min\\{ n \\ge 1 \\mid m^n \\cdot a = a \\}, \\text{ если существует, иначе } 0. $$ \\\\ (на деле period(m,a) = \\minimalPeriod (\\lambda x. m \\cdot x) a)$$
Lean4
/-- The period of a multiplicative action of `g` on `a` is the smallest positive `n` such that
`g ^ n • a = a`, or `0` if such an `n` does not exist.
-/
@[to_additive /-- The period of an additive action of `g` on `a` is the smallest positive `n`
such that `(n • g) +ᵥ a = a`, or `0` if such an `n` does not exist. -/
]
noncomputable def period (m : M) (a : α) : ℕ :=
minimalPeriod (fun x => m • x) a
