nonZeroDivisorsLeft_eq_right — Mathlib

English

In a commutative monoid with zero, the left non-zero divisors coincide with the right non-zero divisors: nonZeroDivisorsLeft M = nonZeroDivisorsRight M.

Русский

Пусть M — коммутативная моноида с нулём. Тогда множества слева и справа не нулевых делителей совпадают: nonZeroDivisorsLeft(M) = nonZeroDivisorsRight(M).

LaTeX

$$$\operatorname{nonZeroDivisorsLeft}(M_0) = \operatorname{nonZeroDivisorsRight}(M_0)$$$

Lean4

theorem nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
    nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by ext x; simp [mul_comm x]

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