period_eq_minimalPeriod — Mathlib

English

For a monoid action of M on α, the period of m on a equals the minimal period of the orbit map if equal to the minimal period value; i.e., period m a = minimalPeriod (·) a.

Русский

Для действия моноида M на α период m на a равен минимальному периоду орбитального отображения, то есть period(m,a) = minimalPeriod (множество) a.

LaTeX

$$$ \\mathrm{period}(m,a) = \\mathrm{minimalPeriod}\\ (\\lambda x. m \\cdot x)\\ a $$$

Lean4

/-- `MulAction.period m a` is definitionally equal to `Function.minimalPeriod (m • ·) a`. -/
@[to_additive /-- `AddAction.period m a` is definitionally equal to
    `Function.minimalPeriod (m +ᵥ ·) a` -/
    ]
theorem period_eq_minimalPeriod {m : M} {a : α} : MulAction.period m a = minimalPeriod (fun x => m • x) a :=
  rfl

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