coe_ne_zero — Mathlib

English

The coercion from the non-zero divisors to the ambient monoid preserves nonzeroness: if x ∈ M⁰, then (x) ≠ 0.

Русский

Коэрцирование из области не нулевых делителей в моноид сохраняет ненулевость: если x ∈ M⁰, то x ≠ 0.

LaTeX

$$$ (x : M_0) \neq 0 \quad \text{for } x \in M_0^{0}$$$

Lean4

@[simp]
theorem coe_ne_zero (x : M₀⁰) : (x : M₀) ≠ 0 :=
  nonZeroDivisors.ne_zero x.2

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