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
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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 lean4#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 lean4#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.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
Instances
An associative but not-necessarily unital semiring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
Instances
A unital but not-necessarily-associative semiring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
Instances
A not-necessarily-unital, not-necessarily-associative ring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- mul : α → α → α
Instances
An associative but not-necessarily unital ring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- mul : α → α → α
Instances
A unital but not-necessarily-associative ring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
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.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
Instances
A Ring
is a Semiring
with negation making it an additive group.
- add : R → R → R
- zero : R
- nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : R → R → R
- one : R
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : R → R
- sub : R → R → R
- sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
- zsmul_zero' : ∀ (a : R), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : R), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : R), -a + a = 0
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
Instances
Semirings #
A not-necessarily-unital, not-necessarily-associative, but commutative semiring.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
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
).
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
Instances
A commutative semiring is a semiring with commutative multiplication.
- add : R → R → R
- zero : R
- nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : R → R → R
- one : R
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = Semiring.npow n x * x
Instances
Equations
- CommSemiring.toNonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯
Equations
- CommSemiring.toCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯
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 = NegZeroClass.mk ⋯
Rings #
Equations
- NonUnitalNonAssocRing.toHasDistribNeg = HasDistribNeg.mk ⋯ ⋯
Equations
- Ring.toNonUnitalRing = NonUnitalRing.mk ⋯
Equations
- Ring.toNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The instance from Ring
to Semiring
happens often in linear algebra, for which all the basic
definitions are given in terms of semirings, but many applications use rings or fields. We increase
a little bit its priority above 100 to try it quickly, but remaining below the default 1000 so that
more specific instances are tried first.
Equations
- instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Semiring.npow ⋯ ⋯
A non-unital non-associative commutative ring is a NonUnitalNonAssocRing
with commutative
multiplication.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- mul : α → α → α
Instances
A non-unital commutative ring is a NonUnitalRing
with commutative multiplication.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- mul : α → α → α
Instances
Equations
- NonUnitalCommRing.toNonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯
A commutative ring is a ring with commutative multiplication.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : α), -a + a = 0
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
Instances
Equations
- CommRing.toCommSemiring = CommSemiring.mk ⋯
Equations
- CommRing.toNonUnitalCommRing = NonUnitalCommRing.mk ⋯
Equations
- CommRing.toAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯
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 α]
.
- exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y