minimalPeriod_eq_one_iff_fixedBy — Mathlib

English

For a ∈ α and g ∈ G, the minimal period of the map x ↦ g • x at a equals 1 if and only if a is fixed by g.

Русский

Для a ∈ α и g ∈ G минимальная периодичность отображения x ↦ g • x в точке a равна единице тогда и только тогда, когда a фиксируется g.

LaTeX

$$$\text{minimalPeriod}(\lambda x. g \cdot x) \ a = 1 \iff a \in fixedBy(α, g)$$$

Lean4

@[to_additive minimalPeriod_eq_one_iff_fixedBy]
theorem minimalPeriod_eq_one_iff_fixedBy {a : α} {g : G} :
    Function.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ fixedBy α g :=
  Function.minimalPeriod_eq_one_iff_isFixedPt

Похожие утверждения