nonZeroDivisorsLeft_eq_nonZeroDivisors

English

In a commutative setting with zero, the left and the standard nonZeroDivisors coincide: nonZeroDivisorsLeft M0 = nonZeroDivisors M0.

Русский

В коммутативном случае с нулём левый и обычный набор ненулевых делителей совпадают: nonZeroDivisorsLeft M0 = nonZeroDivisors M0.

LaTeX

$$nonZeroDivisorsLeft M0 = nonZeroDivisors M0$$

Lean4

theorem nonZeroDivisorsLeft_eq_nonZeroDivisors : nonZeroDivisorsLeft M₀ = nonZeroDivisors M₀ := by
  rw [nonZeroDivisors, nonZeroDivisorsLeft_eq_right, inf_idem]

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