ne_zero — Mathlib

English

In a nontrivial monoid with zero, any unit has nonzero underlying value.

Русский

В ненулевом моноиде с нулём любой элемент-разность (единица) имеет ненулевое базовое значение.

LaTeX

$$$[\text{Nontrivial } M_0]\Rightarrow (u: M_0^\times) \, (u: M_0) \neq 0$$$

Lean4

/-- An element of the unit group of a nonzero monoid with zero represented as an element
of the monoid is nonzero. -/
@[simp]
theorem ne_zero [Nontrivial M₀] (u : M₀ˣ) : (u : M₀) ≠ 0 :=
  left_ne_zero_of_mul_eq_one u.mul_inv

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