Semirings and rings #
This file defines semirings, rings and domains. This is analogous to Algebra.Group.Defs
and
Algebra.Group.Basic
, the difference being that the former is about +
and *
separately, while
the present file is about their interaction.
Main definitions #
Distrib
: Typeclass for distributivity of multiplication over addition.HasDistribNeg
: Typeclass for commutativity of negation and multiplication. This is useful when dealing with multiplicative submonoids which are closed under negation without being closed under addition, for exampleUnits
.(NonUnital)(NonAssoc)(Semi)Ring
: Typeclasses for possibly non-unital or non-associative rings and semirings. Some combinations are not defined yet because they haven't found use. For Lie Rings, there is a type synonymCommutatorRing
defined inMathlib/Algebra/Algebra/NonUnitalHom.lean
turning the bracket into a multiplication so that the instanceinstNonUnitalNonAssocSemiringCommutatorRing
can be defined.
Tags #
Semiring
, CommSemiring
, Ring
, CommRing
, domain, IsDomain
, nonzero, units
Previously an import dependency on Mathlib/Algebra/Group/Basic.lean
had crept in.
In general, the .Defs
files in the basic algebraic hierarchy should only depend on earlier .Defs
files, without importing .Basic
theory development.
These assert_not_exists
statements guard against this returning.
Classes of semirings and rings #
We make sure that the canonical path from NonAssocSemiring
to Ring
passes through Semiring
,
as this is a path which is followed all the time in linear algebra where the defining semilinear map
σ : R →+* S
depends on the NonAssocSemiring
structure of R
and S
while the module
definition depends on the Semiring
structure.
It is not currently possible to adjust priorities by hand (see https://github.com/leanprover/lean4/issues/2115). Instead, the last
declared instance is used, so we make sure that Semiring
is declared after NonAssocRing
, so
that Semiring -> NonAssocSemiring
is tried before NonAssocRing -> NonAssocSemiring
.
TODO: clean this once https://github.com/leanprover/lean4/issues/2115 is fixed
A not-necessarily-unital, not-necessarily-associative semiring. See CommutatorRing
and the
documentation thereof in case you need a NonUnitalNonAssocSemiring
instance on a Lie ring
or a Lie algebra.
Instances
An associative but not-necessarily unital semiring.
Instances
A unital but not-necessarily-associative semiring.
Instances
A not-necessarily-unital, not-necessarily-associative ring.
Instances
An associative but not-necessarily unital ring.
Instances
A unital but not-necessarily-associative ring.
Instances
A Semiring
is a type with addition, multiplication, a 0
and a 1
where addition is
commutative and associative, multiplication is associative and left and right distributive over
addition, and 0
and 1
are additive and multiplicative identities.
Instances
Semirings #
A not-necessarily-unital, not-necessarily-associative, but commutative semiring.
Instances
A non-unital commutative semiring is a NonUnitalSemiring
with commutative multiplication.
In other words, it is a type with the following structures: additive commutative monoid
(AddCommMonoid
), commutative semigroup (CommSemigroup
), distributive laws (Distrib
), and
multiplication by zero law (MulZeroClass
).
Instances
A commutative semiring is a semiring with commutative multiplication.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- CommSemiring.toCommMonoidWithZero = { toCommMonoid := inferInstanceAs (CommMonoid α), toZero := AddMonoid.toZero, zero_mul := ⋯, mul_zero := ⋯ }
Typeclass for a negation operator that distributes across multiplication.
This is useful for dealing with submonoids of a ring that contain -1
without having to duplicate
lemmas.
- neg : α → α
Negation is left distributive over multiplication
Negation is right distributive over multiplication
Instances
An element of a ring multiplied by the additive inverse of one is the element's additive inverse.
The additive inverse of one multiplied by an element of a ring is the element's additive inverse.
Equations
- MulZeroClass.negZeroClass = { toZero := inferInstanceAs (Zero α), toNeg := InvolutiveNeg.toNeg, neg_zero := ⋯ }
Rings #
Equations
- NonUnitalNonAssocRing.toHasDistribNeg = { toNeg := SubNegMonoid.toNeg, neg_neg := ⋯, neg_mul := ⋯, mul_neg := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A non-unital non-associative commutative ring is a NonUnitalNonAssocRing
with commutative
multiplication.
Instances
A non-unital commutative ring is a NonUnitalRing
with commutative multiplication.
Instances
Equations
- One or more equations did not get rendered due to their size.
A commutative ring is a ring with commutative multiplication.
Instances
Equations
- CommRing.toCommSemiring = { toSemiring := Ring.toSemiring, mul_comm := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A domain is a nontrivial semiring such that multiplication by a non zero element
is cancellative on both sides. In other words, a nontrivial semiring R
satisfying
∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c
and
∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c
.
This is implemented as a mixin for Semiring α
.
To obtain an integral domain use [CommRing α] [IsDomain α]
.