# Documentation

Mathlib.GroupTheory.Submonoid.ZeroDivisors

# Zero divisors #

## Main definitions #

• nonZeroDivisorsLeft: the elements of a MonoidWithZero that are not left zero divisors.
• nonZeroDivisorsRight: the elements of a MonoidWithZero that are not right zero divisors.
def nonZeroDivisorsLeft (M₀ : Type u_1) [] :

The collection of elements of a MonoidWithZero that are not left zero divisors form a Submonoid.

Instances For
@[simp]
theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [] {x : M₀} :
∀ (y : M₀), y * x = 0y = 0
def nonZeroDivisorsRight (M₀ : Type u_1) [] :

The collection of elements of a MonoidWithZero that are not right zero divisors form a Submonoid.

Instances For
@[simp]
theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [] {x : M₀} :
∀ (y : M₀), x * y = 0y = 0
theorem nonZeroDivisorsLeft_eq_right (M₀ : Type u_1) [] :
@[simp]
theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [] [] [] :
↑() = {x | x 0}
@[simp]
theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [] [] [] :
↑() = {x | x 0}