orderOf_pos — Mathlib

English

If Mˣ is finite, then the order of χ is positive: orderOf χ > 0.

Русский

Если Mˣ конечен, то порядок χ положителен: orderOf χ > 0.

LaTeX

$$0 < orderOf χ$$

Lean4

/-- A multiplicative character on a commutative monoid with finitely many units
has finite (= positive) order. -/
theorem orderOf_pos [Finite Mˣ] (χ : MulChar M R) : 0 < orderOf χ :=
  by
  cases nonempty_fintype Mˣ
  apply IsOfFinOrder.orderOf_pos
  exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

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