isPeriodicPt_smul_iff — Mathlib

English

For a ∈ α and m ∈ M, a is periodic with period n under the action m • · if and only if m^n • a = a.

Русский

Пусть a ¦ α, m ∈ M. Точка a периодична с периодом n по действию m • · тогда и только тогда, когда m^n • a = a.

LaTeX

$$$ \\mathrm{IsPeriodicPt}\\ (m \\cdot)\\ n\\ a \\iff m^n \\cdot a = a $$$

Lean4

@[to_additive]
theorem isPeriodicPt_smul_iff {m : M} {a : α} {n : ℕ} : IsPeriodicPt (m • ·) n a ↔ m ^ n • a = a := by
  rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]

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