minimalPeriod_pos — Mathlib

English

If the orbit is finite, then minimalPeriod is nonzero.

Русский

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

LaTeX

$$$ [\text{Finite }\mathcal{O}] \Rightarrow \minPeriod(a\cdot) b \neq 0 $$$

Lean4

@[to_additive]
instance minimalPeriod_pos [Finite <| orbit (zpowers a) b] : NeZero <| minimalPeriod (a • ·) b :=
  ⟨by
    cases nonempty_fintype (orbit (zpowers a) b)
    haveI : Nonempty (orbit (zpowers a) b) := (nonempty_orbit b).to_subtype
    rw [minimalPeriod_eq_card]
    exact Fintype.card_ne_zero⟩

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