orderOf_zero — Mathlib

English

In a nontrivial MonoidWithZero, the order of 0 is 0.

Русский

В ненулевом моноиде с нулём порядок элемента 0 равен 0.

LaTeX

$$orderOf (0 : M₀) = 0$$

Lean4

/-- In a nontrivial monoid with zero, the order of the zero element is zero. -/
@[simp]
theorem orderOf_zero (M₀ : Type*) [MonoidWithZero M₀] [Nontrivial M₀] : orderOf (0 : M₀) = 0 :=
  by
  rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one]
  simp +contextual [ne_of_gt]

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