coe_nonZeroDivisorsLeft_eq — Mathlib

English

For a monoid with zero with NoZeroDivisors and Nontrivial, the left non-zero divisors are precisely the nonzero elements: nonZeroDivisorsLeft M0 = { x : M0 | x ≠ 0 }.

Русский

Пусть M0 — моноид с нулём, удовлетворяющий NoZeroDivisors и не тривиален. Тогда слева не нулевые делители совпадают с ненулевыми элементами: nonZeroDivisorsLeft M0 = { x : M0 | x ≠ 0 }.

LaTeX

$$$\operatorname{nonZeroDivisorsLeft}(M_0) = \{ x : M_0 \mid x \neq 0 \}$$$

Lean4

@[simp]
theorem coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] : nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0} :=
  by
  ext x
  simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, Set.mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by simp_all⟩
  contrapose! h
  exact ⟨1, Or.inl h, one_ne_zero⟩

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