minimalPeriod_eq_card — Mathlib

English

When the orbit is finite, the minimal period equals the cardinality of the orbit.

Русский

Если орбита конечна, минимальный период равен мощности орбиты.

LaTeX

$$$ [\text{Finite }(\mathrm{orbit}(zpowers a) b)] \Rightarrow \minPeriod(a\cdot) b = |\mathrm{orbit}(zpowers a) b| $$$

Lean4

@[to_additive]
theorem minimalPeriod_eq_card [Fintype (orbit (zpowers a) b)] :
    minimalPeriod (a • ·) b = Fintype.card (orbit (zpowers a) b) := by
  rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), ZMod.card]

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