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.
Tags #
Semiring
, CommSemiring
, Ring
, CommRing
, domain, IsDomain
, nonzero, units
distrib
class #
Multiplication is left distributive over addition
Multiplication is right distributive over addition
A typeclass stating that multiplication is left and right distributive over addition.
Instances
Semirings #
Multiplication is left distributive over addition
Multiplication is right distributive over addition
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A not-necessarily-unital, not-necessarily-associative semiring.
Instances
One is a right neutral element for multiplication
- toNatCast : NatCast α
The canonical map
ℕ → R→ R
sends0 : ℕ
to0 : R
.natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝The canonical map
ℕ → R→ R
is a homomorphism.natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝
A unital but not-necessarily-associative semiring.
Instances
One is a right neutral element for multiplication
- toNatCast : NatCast α
The canonical map
ℕ → R→ R
sends0 : ℕ
to0 : R
.natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝The canonical map
ℕ → R→ R
is a homomorphism.natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝Raising to the power of a natural number.
npow : ℕ → α → αRaising to the power
(0 : ℕ)
gives1
.Raising to the power
(n + 1 : ℕ)
behaves as expected.
Instances
Multiplication is commutative in a commutative semigroup.
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
Equations
- CommSemiring.toNonUnitalCommSemiring = let src := inferInstanceAs (CommMonoid α); let src_1 := inferInstanceAs (CommSemiring α); NonUnitalCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- One or more equations did not get rendered due to their size.
Negation is left distributive over multiplication
Negation is right distributive over multiplication
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.
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 = let src := inferInstanceAs (Zero α); let src_1 := inferInstanceAs (InvolutiveNeg α); NegZeroClass.mk (_ : -0 = 0)
Rings #
Multiplication is left distributive over addition
Multiplication is right distributive over addition
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A not-necessarily-unital, not-necessarily-associative ring.
Instances
- toNatCast : NatCast α
The canonical map
ℕ → R→ R
sends0 : ℕ
to0 : R
.natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝The canonical map
ℕ → R→ R
is a homomorphism.natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝- toIntCast : IntCast α
The canonical homorphism
ℤ → R→ R
agrees with the one fromℕ → R→ R
onℕ
.intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝The canonical homorphism
ℤ → R→ R
for negative values is just the negation of the values of the canonical homomorphismℕ → R→ R
.intCast_negSucc : autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) _auto✝
A unital but not-necessarily-associative ring.
Instances
- zsmul : ℤ → R → R
- toIntCast : IntCast R
The canonical homorphism
ℤ → R→ R
agrees with the one fromℕ → R→ R
onℕ
.intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝The canonical homorphism
ℤ → R→ R
for negative values is just the negation of the values of the canonical homomorphismℕ → R→ R
.intCast_negSucc : autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) _auto✝
Instances
A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.
Multiplication is commutative in a commutative semigroup.
A non-unital commutative ring is a NonUnitalRing
with commutative multiplication.
Instances
Equations
- NonUnitalCommRing.toNonUnitalCommSemiring = NonUnitalCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- CommRing.toCommSemiring = CommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- CommRing.toNonUnitalCommRing = NonUnitalCommRing.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- CommRing.toAddCommGroupWithOne = AddCommGroupWithOne.mk
A domain is a nontrivial semiring such 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∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c≠ 0 → a * b = a * c → b = c→ a * b = a * c → b = c→ b = c
and
∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c≠ 0 → a * b = c * b → a = c→ a * b = c * b → a = c→ a = c
.
This is implemented as a mixin for Semiring α
.
To obtain an integral domain use [CommRing α] [IsDomain α]
.