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₀ = { 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
    theorem nmem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {r : M₀} :
    rnonZeroDivisorsLeft M₀ {s : M₀ | s * r = 0 s 0}.Nonempty
    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₀ = { 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
      theorem nmem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {r : M₀} :
      rnonZeroDivisorsRight M₀ {s : M₀ | r * s = 0 s 0}.Nonempty
      @[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 = { 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_1) [MonoidWithZero R] (M : Type u_2) [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
          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_1} [MonoidWithZero M] {r : M} :
              r nonZeroDivisors M ∀ (x : M), x * r = 0x = 0
              theorem nmem_nonZeroDivisors_iff {M : Type u_1} [MonoidWithZero M] {r : M} :
              rnonZeroDivisors M {s : M | s * r = 0 s 0}.Nonempty
              theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_1} [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_1} [MonoidWithZero M] {x : M} {c : (nonZeroDivisors M)} :
              x * c = 0 x = 0
              theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_3} [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_3} [CommMonoidWithZero M₁] {c : (nonZeroDivisors M₁)} {x : M₁} :
              c * x = 0 x = 0
              theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_4} [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_4} [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_5} [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_5} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              c * x = c * y x = y
              theorem dvd_cancel_right_mem_nonZeroDivisors {R' : Type u_5} [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_5} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              x * c y * c x y
              theorem dvd_cancel_left_mem_nonZeroDivisors {R' : Type u_5} [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_5} [CommRing R'] {x : R'} {y : R'} {c : (nonZeroDivisors R')} :
              c * x c * y x y
              theorem nonZeroDivisors.ne_zero {M : Type u_1} [MonoidWithZero M] [Nontrivial M] {x : M} (hx : x nonZeroDivisors M) :
              x 0
              @[simp]
              theorem nonZeroDivisors.coe_ne_zero {M : Type u_1} [MonoidWithZero M] [Nontrivial M] (x : (nonZeroDivisors M)) :
              x 0
              theorem mul_mem_nonZeroDivisors {M₁ : Type u_3} [CommMonoidWithZero M₁] {a : M₁} {b : M₁} :
              theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_7} [GroupWithZero G₀] {x : G₀} (hx : x nonZeroDivisors G₀) :
              theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} [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_1} [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_1} {M' : Type u_2} {F : Type u_6} [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_1} {M' : Type u_2} {F : Type u_6} [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) :

              In a finite ring, an element is a unit iff it is a non-zero-divisor.

              theorem mem_nonZeroSMulDivisors_iff {R : Type u_1} {M : Type u_2} [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.

              @[simp]
              theorem val_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) :
              (unitsNonZeroDivisorsEquiv.symm u) = u
              @[simp]
              theorem val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) :
              (unitsNonZeroDivisorsEquiv.symm u)⁻¹ = u⁻¹
              @[simp]
              theorem unitsNonZeroDivisorsEquiv_apply {M₀ : Type u_1} [MonoidWithZero M₀] :
              ∀ (a : (↥(nonZeroDivisors M₀))ˣ), unitsNonZeroDivisorsEquiv a = (↑(Units.map (nonZeroDivisors M₀).subtype)).toFun a
              def unitsNonZeroDivisorsEquiv {M₀ : Type u_1} [MonoidWithZero M₀] :
              (↥(nonZeroDivisors M₀))ˣ ≃* M₀ˣ

              The units of the monoid of non-zero divisors of M₀ are equivalent to the units of M₀.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem nonZeroDivisors.associated_coe {M₀ : Type u_1} [MonoidWithZero M₀] {a : (nonZeroDivisors M₀)} {b : (nonZeroDivisors M₀)} :
                Associated a b Associated a b

                The non-zero divisors of associates of a monoid with zero M₀ are isomorphic to the associates of the non-zero divisors of M₀ under the map ⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem associatesNonZeroDivisorsEquiv_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : a nonZeroDivisors (Associates M₀)) :
                  associatesNonZeroDivisorsEquiv a, ha = a,
                  @[simp]
                  theorem associatesNonZeroDivisorsEquiv_symm_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : a nonZeroDivisors M₀) :
                  associatesNonZeroDivisorsEquiv.symm a, ha = a,