coe_nonZeroDivisorsRight_eq — Mathlib

English

Similarly, NoZeroDivisors implies that right non-zero divisors are exactly the nonzero elements: nonZeroDivisorsRight M0 = { x : M0 | x ≠ 0 }.

Русский

Аналогично, если нет нулевых делителей, правая часть не нулевых делителей совпадает с ненулевыми элементами: nonZeroDivisorsRight M0 = { x : M0 | x ≠ 0 }.

LaTeX

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

Lean4

@[simp]
theorem coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] : nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0} :=
  by
  ext x
  simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, forall_eq_or_imp, true_and, Set.mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩
  contrapose! h
  exact ⟨1, h, one_ne_zero⟩

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