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:
R⁰
for the submonoid of non-zero-divisors ofR
, in the localenonZeroDivisors
.R⁰[M]
for the submonoid of non-zero smul-divisors ofR
with respect toM
, in the localenonZeroSMulDivisors
Use the statement open scoped nonZeroDivisors nonZeroSMulDivisors
to access this notation in
your own code.
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 = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
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 = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The submonoid of non-zero-divisors of a MonoidWithZero
R
.
Equations
- nonZeroDivisors R = { carrier := {x : R | ∀ (z : R), z * x = 0 → z = 0}, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The notation for the submonoid of non-zerodivisors.
Equations
- nonZeroDivisors.«term_⁰» = Lean.ParserDescr.trailingNode `nonZeroDivisors.term_⁰ 9000 0 (Lean.ParserDescr.symbol "⁰")
Instances For
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 = { carrier := {r : R | ∀ (m : M), r • m = 0 → m = 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
In a finite ring, an element is a unit iff it is a non-zero-divisor.
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.
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
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.