orderOf_eq_zero_iff_eq_zero — Mathlib

English

For a GroupWithZero G0 finite, orderOf a = 0 iff a = 0.

Русский

Для конечной группы с нулём G0 порядок элемента a равен 0 тогда и только тогда, когда a = 0.

LaTeX

$$orderOf a = 0 \leftrightarrow a = 0$$

Lean4

theorem orderOf_eq_zero_iff_eq_zero {G₀ : Type*} [GroupWithZero G₀] [Finite G₀] {a : G₀} : orderOf a = 0 ↔ a = 0 := by
  -- Prove an instance inline to avoid extra imports.
    -- TODO: move this instance elsewhere?

  have : Finite G₀ˣ := .of_injective _ Units.val_injective
  simp [isOfFinOrder_iff_isUnit]

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