Documentation

Mathlib.GroupTheory.Submonoid.ZeroDivisors

Zero divisors #

Main definitions #

source
def nonZeroDivisorsLeft (M₀ : Type u_1) [MonoidWithZero M₀] :
Submonoid M₀

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} :
    x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (y : M₀), y * x = 0 → y = 0
    source
    def nonZeroDivisorsRight (M₀ : Type u_1) [MonoidWithZero M₀] :
    Submonoid M₀

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} :
      x ∈ nonZeroDivisorsRight M₀ ↔ ∀ (y : M₀), x * y = 0 → y = 0
      source
      theorem nonZeroDivisorsLeft_eq_right (M₀ : Type u_1) [CommMonoidWithZero M₀] :
      nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
      source
      @[simp]
      theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] :
      ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
      source
      @[simp]
      theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] :
      ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}