Division (semi)rings and (semi)fields #
This file introduces fields and division rings (also known as skewfields) and proves some basic
statements about them. For a more extensive theory of fields, see the FieldTheory folder.
Main definitions #
DivisionSemiring: Nontrivial semiring with multiplicative inverses for nonzero elements.DivisionRing: : Nontrivial ring with multiplicative inverses for nonzero elements.Semifield: Commutative division semiring.Field: Commutative division ring.IsField: Predicate on a (semi)ring that it is a (semi)field, i.e. that the multiplication is commutative, that it has more than one element and that all non-zero elements have a multiplicative inverse. In contrast toField, which contains the data of a function associating to an element of the field its multiplicative inverse, this predicate only assumes the existence and can therefore more easily be used to e.g. transfer along ring isomorphisms.
Implementation details #
By convention 0⁻¹ = 0⁻¹ = 0 in a field or division ring. This is due to the fact that working with total
functions has the advantage of not constantly having to check that x ≠ 0≠ 0 when writing x⁻¹⁻¹. With
this convention in place, some statements like (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹⁻¹ = a * c⁻¹ + b * c⁻¹⁻¹ + b * c⁻¹⁻¹ still remain
true, while others like the defining property a * a⁻¹ = 1⁻¹ = 1 need the assumption a ≠ 0≠ 0. If you are
a beginner in using Lean and are confused by that, you can read more about why this convention is
taken in Kevin Buzzard's
blogpost
A division ring or field is an example of a GroupWithZero. If you cannot find
a division ring / field lemma that does not involve +, you can try looking for
a GroupWithZero lemma instead.
Tags #
field, division ring, skew field, skew-field, skewfield
The default definition of the coercion (↑(a : ℚ) : K)↑(a : ℚ) : K) for a division ring K
is defined as (a / b : K) = (a : K) * (b : K)⁻¹⁻¹.
Use coe instead of Rat.castRec for better definitional behaviour.
Equations
- Rat.castRec x = match x with | Rat.mk' a b => ↑a * (↑b)⁻¹
The default definition of the scalar multiplication (a : ℚ) • (x : K) for a division ring K
is given by a • x = (↑ a) * x↑ a) * x.
Use (a : ℚ) • (x : K) instead of qsmulRec for better definitional behaviour.
The power operation:
a ^ n = a * ··· * a;a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹(ntimes)zpow : ℤ → α → αa ^ 0 = 1a ^ (n + 1) = a * a ^ na ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹- toNontrivial : Nontrivial α
The inverse of
0in a group with zero is0.Every nonzero element of a group with zero is invertible.
A DivisionSemiring is a Semiring with multiplicative inverses for nonzero elements.
Instances
a ^ 0 = 1a ^ (n + 1) = a * a ^ na ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹- toNontrivial : Nontrivial K
- toRatCast : RatCast K
For a nonzero
a,a⁻¹⁻¹is a right multiplicative inverse.We define the inverse of
0to be0.However
ratCastis defined, propositionally it must be equal toa * b⁻¹⁻¹.Multiplication by a rational number.
qsmul : ℚ → K → KHowever
qsmulis defined, propositionally it must be equal to multiplication byratCast.
A DivisionRing is a Ring with multiplicative inverses for nonzero elements.
An instance of DivisionRing K includes maps ratCast : ℚ → K→ K and qsmul : ℚ → K → K→ K → K→ K.
If the division ring has positive characteristic p, we define ratCast (1 / p) = 1 / 0 = 0
for consistency with our division by zero convention.
The fields ratCast and qsmul are needed to implement the
algebraRat [DivisionRing K] : Algebra ℚ K instance, since we need to control the specific
definitions for some special cases of K (in particular K = ℚ itself).
See also Note [forgetful inheritance].
Instances
The power operation:
a ^ n = a * ··· * a;a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹(ntimes)zpow : ℤ → α → αa ^ 0 = 1a ^ (n + 1) = a * a ^ na ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹- toNontrivial : Nontrivial α
The inverse of
0in a group with zero is0.Every nonzero element of a group with zero is invertible.
A Semifield is a CommSemiring with multiplicative inverses for nonzero elements.
Instances
a ^ 0 = 1a ^ (n + 1) = a * a ^ na ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹- toNontrivial : Nontrivial K
- toRatCast : RatCast K
For a nonzero
a,a⁻¹⁻¹is a right multiplicative inverse.We define the inverse of
0to be0.However
ratCastis defined, propositionally it must be equal toa * b⁻¹⁻¹.Multiplication by a rational number.
qsmul : ℚ → K → KHowever
qsmulis defined, propositionally it must be equal to multiplication byratCast.
A Field is a CommRing with multiplicative inverses for nonzero elements.
An instance of Field K includes maps ratCast : ℚ → K→ K and qsmul : ℚ → K → K→ K → K→ K.
If the field has positive characteristic p, we define ratCast (1 / p) = 1 / 0 = 0
for consistency with our division by zero convention.
The fields ratCast and qsmul are needed to implement the
algebraRat [DivisionRing K] : Algebra ℚ K instance, since we need to control the specific
definitions for some special cases of K (in particular K = ℚ itself).
See also Note [forgetful inheritance].
Instances
Equations
- Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
For a semiring to be a field, it must have two distinct elements.
exists_pair_ne : ∃ x y, x ≠ yFields are commutative.
Nonzero elements have multiplicative inverses.
A predicate to express that a (semi)ring is a (semi)field.
This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms. Additionaly, this is useful when trying to prove that a particular ring structure extends to a (semi)field.
Instances For
For each field, and for each nonzero element of said field, there is a unique inverse.
Since IsField doesn't remember the data of an inv function and as such,
a lemma that there is a unique inverse could be useful.