Documentation

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Non-zero divisors and smul-divisors #

In this file we define the submonoid nonZeroDivisors and nonZeroSMulDivisors of a MonoidWithZero. We also define nonZeroDivisorsLeft and nonZeroDivisorsRight for non-commutative monoids.

Notations #

This file declares the notations:

Use the statement open scoped nonZeroDivisors nonZeroSMulDivisors to access this notation in your own code.

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

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

Equations
  • nonZeroDivisorsLeft M₀ = { toSubsemigroup := { carrier := {x : M₀ | ∀ (y : M₀), y * x = 0y = 0}, mul_mem' := }, one_mem' := }
Instances For
    @[simp]
    theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} :
    x nonZeroDivisorsLeft M₀ ∀ (y : M₀), y * x = 0y = 0
    def nonZeroDivisorsRight (M₀ : Type u_1) [MonoidWithZero M₀] :

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

    Equations
    • nonZeroDivisorsRight M₀ = { toSubsemigroup := { carrier := {x : M₀ | ∀ (y : M₀), x * y = 0y = 0}, mul_mem' := }, one_mem' := }
    Instances For
      @[simp]
      theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} :
      x nonZeroDivisorsRight M₀ ∀ (y : M₀), x * y = 0y = 0
      @[simp]
      theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] :
      (nonZeroDivisorsLeft M₀) = {x : M₀ | x 0}
      @[simp]
      theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] :
      (nonZeroDivisorsRight M₀) = {x : M₀ | x 0}

      The submonoid of non-zero-divisors of a MonoidWithZero R.

      Equations
      • nonZeroDivisors R = { toSubsemigroup := { carrier := {x : R | ∀ (z : R), z * x = 0z = 0}, mul_mem' := }, one_mem' := }
      Instances For

        The notation for the submonoid of non-zerodivisors.

        Equations
        Instances For
          def nonZeroSMulDivisors (R : Type u_2) [MonoidWithZero R] (M : Type u_3) [Zero M] [MulAction R M] :

          Let R be a monoid with zero and M an additive monoid with an R-action, then the collection of non-zero smul-divisors forms a submonoid. These elements are also called M-regular.

          Equations
          • nonZeroSMulDivisors R M = { toSubsemigroup := { carrier := {r : R | ∀ (m : M), r m = 0m = 0}, mul_mem' := }, one_mem' := }
          Instances For

            The notation for the submonoid of non-zero smul-divisors.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem mem_nonZeroDivisors_iff {M : Type u_2} [MonoidWithZero M] {r : M} :
              r nonZeroDivisors M ∀ (x : M), x * r = 0x = 0
              theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_2} [MonoidWithZero M] {x : M} {r : M} (hr : r nonZeroDivisors M) :
              x * r = 0 x = 0
              @[simp]
              theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M : Type u_2} [MonoidWithZero M] {x : M} {c : (nonZeroDivisors M)} :
              x * c = 0 x = 0
              theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_4} [CommMonoidWithZero M₁] {r : M₁} {x : M₁} (hr : r nonZeroDivisors M₁) :
              r * x = 0 x = 0
              @[simp]
              theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₁ : Type u_4} [CommMonoidWithZero M₁] {c : (nonZeroDivisors M₁)} {x : M₁} :
              c * x = 0 x = 0
              theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_5} [Ring R] {x : R} {y : R} {r : R} (hr : r nonZeroDivisors R) :
              x * r = y * r x = y
              theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_5} [Ring R] {x : R} {y : R} {c : (nonZeroDivisors R)} :
              x * c = y * c x = y
              @[simp]
              theorem mul_cancel_left_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r nonZeroDivisors R') :
              r * x = r * y x = y
              theorem mul_cancel_left_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              c * x = c * y x = y
              theorem dvd_cancel_right_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r nonZeroDivisors R') :
              x * r y * r x y
              theorem dvd_cancel_right_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              x * c y * c x y
              theorem dvd_cancel_left_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r nonZeroDivisors R') :
              r * x r * y x y
              theorem dvd_cancel_left_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              c * x c * y x y
              theorem nonZeroDivisors.ne_zero {M : Type u_2} [MonoidWithZero M] [Nontrivial M] {x : M} (hx : x nonZeroDivisors M) :
              x 0
              theorem mul_mem_nonZeroDivisors {M₁ : Type u_4} [CommMonoidWithZero M₁] {a : M₁} {b : M₁} :
              theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_8} [GroupWithZero G₀] {x : G₀} (hx : x nonZeroDivisors G₀) :
              theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_2} [MonoidWithZero M] [NoZeroDivisors M] {x : M} {y : M} (hnx : x 0) (hxy : y * x = 0) :
              y = 0
              theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {M : Type u_2} [MonoidWithZero M] [NoZeroDivisors M] {x : M} {y : M} (hnx : x 0) (hxy : x * y = 0) :
              y = 0
              theorem map_ne_zero_of_mem_nonZeroDivisors {M : Type u_2} {M' : Type u_3} {F : Type u_7} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [Nontrivial M] [ZeroHomClass F M M'] (g : F) (hg : Function.Injective g) {x : M} (h : x nonZeroDivisors M) :
              g x 0
              theorem map_mem_nonZeroDivisors {M : Type u_2} {M' : Type u_3} {F : Type u_7} [MonoidWithZero M] [MonoidWithZero M'] [FunLike F M M'] [Nontrivial M] [NoZeroDivisors M'] [ZeroHomClass F M M'] (g : F) (hg : Function.Injective g) {x : M} (h : x nonZeroDivisors M) :
              @[deprecated Multiset.prod_eq_zero_iff]
              theorem prod_zero_iff_exists_zero {M₁ : Type u_4} [CommMonoidWithZero M₁] [NoZeroDivisors M₁] [Nontrivial M₁] {s : Multiset M₁} :
              Multiset.prod s = 0 ∃ (r : M₁) (_ : r s), r = 0
              theorem mem_nonZeroSMulDivisors_iff {R : Type u_2} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulAction R M] {x : R} :
              x nonZeroSMulDivisors R M ∀ (m : M), x m = 0m = 0

              The non-zero -divisors with as right multiplication correspond with the non-zero divisors. Note that the MulOpposite is needed because we defined nonZeroDivisors with multiplication on the right.