periodicPts_add_left — Mathlib

English

In a nonzero ZMod-n-module, translations by any fixed x have every point periodic with period n; i.e., every y is periodic under the map y ↦ x + y with period n.

Русский

В модуле над ZMod n с ненулевой характеристикой любая сдвиговая по фиксированному x транспозиция y ↦ x + y имеет все точки периодическими с периодом n.

LaTeX

$$$\text{periodicPts}(x + \cdot) = \mathrm{Set.univ}$$$

Lean4

theorem periodicPts_add_left [NeZero n] (x : G) : periodicPts (x + ·) = .univ :=
  Set.eq_univ_of_forall fun y ↦ ⟨n, NeZero.pos n, by simpa [char_nsmul_eq_zero, IsPeriodicPt] using isFixedPt_id _⟩

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