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
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
when writing x⁻¹
. With
this convention in place, some statements like (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹
still remain
true, while others like the defining property a * a⁻¹ = 1
need the assumption a ≠ 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 ℚ≥0 → K
for a division semiring K
.
↑q : K
is defined as (q.num : K) / (q.den : K)
.
Do not use this directly (instances of DivisionSemiring
are allowed to override that default for
better definitional properties). Instead, use the coercion.
Instances For
The default definition of the coercion ℚ → K
for a division ring K
.
↑q : K
is defined as (q.num : K) / (q.den : K)
.
Do not use this directly (instances of DivisionRing
are allowed to override that default for
better definitional properties). Instead, use the coercion.
Instances For
A DivisionSemiring
is a Semiring
with multiplicative inverses for nonzero elements.
An instance of DivisionSemiring K
includes maps nnratCast : ℚ≥0 → K
and nnqsmul : ℚ≥0 → K → K
.
Those two fields are needed to implement the DivisionSemiring K → Algebra ℚ≥0 K
instance since we
need to control the specific definitions for some special cases of K
(in particular K = ℚ≥0
itself). See also note [forgetful inheritance].
If the division semiring has positive characteristic p
, our division by zero convention forces
nnratCast (1 / p) = 1 / 0 = 0
.
- add : K → K → K
- zero : K
- nsmul : ℕ → K → K
- nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : K → K → K
- one : K
- natCast : ℕ → K
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → K → K
- npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
- inv : K → K
- div : K → K → K
a / b := a * b⁻¹
- zpow : ℤ → K → K
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : K), DivisionSemiring.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : K), DivisionSemiring.zpow (Int.ofNat n.succ) a = DivisionSemiring.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : K), DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
- nnratCast : ℚ≥0 → K
However
NNRat.cast
is defined, it must be propositionally equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → K → K
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : K), DivisionSemiring.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead.
Instances
However NNRat.cast
is defined, it must be propositionally equal to a / b
.
Do not use this lemma directly. Use NNRat.cast_def
instead.
However qsmul
is defined, it must be propositionally equal to multiplication by Rat.cast
.
Do not use this lemma directly. Use NNRat.smul_def
instead.
A DivisionRing
is a Ring
with multiplicative inverses for nonzero elements.
An instance of DivisionRing K
includes maps ratCast : ℚ → K
and qsmul : ℚ → K → K
.
Those two fields are needed to implement the 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]. Similarly, there are maps nnratCast ℚ≥0 → K
and
nnqsmul : ℚ≥0 → K → K
to implement the DivisionSemiring K → Algebra ℚ≥0 K
instance.
If the division ring has positive characteristic p
, our division by zero convention forces
ratCast (1 / p) = 1 / 0 = 0
.
- add : K → K → K
- zero : K
- nsmul : ℕ → K → K
- nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : K → K → K
- one : K
- natCast : ℕ → K
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → K → K
- npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : K → K
- sub : K → K → K
- zsmul : ℤ → K → K
- zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → K
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : K → K
- div : K → K → K
a / b := a * b⁻¹
- zpow : ℤ → K → K
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : K), DivisionRing.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : K), DivisionRing.zpow (Int.ofNat n.succ) a = DivisionRing.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : K), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
- nnratCast : ℚ≥0 → K
- ratCast : ℚ → K
For a nonzero
a
,a⁻¹
is a right multiplicative inverse.The inverse of
0
is0
by convention.However
NNRat.cast
is defined, it must be equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → K → K
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : K), DivisionRing.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead. However
Rat.cast q
is defined, it must be propositionally equal toq.num / q.den
.Do not use this lemma directly. Use
Rat.cast_def
instead.- qsmul : ℚ → K → K
- qsmul_def : ∀ (a : ℚ) (x : K), DivisionRing.qsmul a x = ↑a * x
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
Rat.cast_def
instead.
Instances
For a nonzero a
, a⁻¹
is a right multiplicative inverse.
The inverse of 0
is 0
by convention.
However NNRat.cast
is defined, it must be equal to a / b
.
Do not use this lemma directly. Use NNRat.cast_def
instead.
However qsmul
is defined, it must be propositionally equal to multiplication by Rat.cast
.
Do not use this lemma directly. Use NNRat.smul_def
instead.
However Rat.cast q
is defined, it must be propositionally equal to q.num / q.den
.
Do not use this lemma directly. Use Rat.cast_def
instead.
However qsmul
is defined, it must be propositionally equal to multiplication by Rat.cast
.
Do not use this lemma directly. Use Rat.cast_def
instead.
Equations
- DivisionRing.toDivisionSemiring = DivisionSemiring.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯
A Semifield
is a CommSemiring
with multiplicative inverses for nonzero elements.
An instance of Semifield K
includes maps nnratCast : ℚ≥0 → K
and nnqsmul : ℚ≥0 → K → K
.
Those two fields are needed to implement the DivisionSemiring K → Algebra ℚ≥0 K
instance since we
need to control the specific definitions for some special cases of K
(in particular K = ℚ≥0
itself). See also note [forgetful inheritance].
If the semifield has positive characteristic p
, our division by zero convention forces
nnratCast (1 / p) = 1 / 0 = 0
.
- add : K → K → K
- zero : K
- nsmul : ℕ → K → K
- nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : K → K → K
- one : K
- natCast : ℕ → K
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → K → K
- npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
- inv : K → K
- div : K → K → K
a / b := a * b⁻¹
- zpow : ℤ → K → K
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : K), Semifield.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : K), Semifield.zpow (Int.ofNat n.succ) a = Semifield.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : K), Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
- nnratCast : ℚ≥0 → K
However
NNRat.cast
is defined, it must be propositionally equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → K → K
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Semifield.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead.
Instances
A Field
is a CommRing
with multiplicative inverses for nonzero elements.
An instance of Field K
includes maps ratCast : ℚ → K
and qsmul : ℚ → K → K
.
Those two fields are needed to implement the 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].
If the field has positive characteristic p
, our division by zero convention forces
ratCast (1 / p) = 1 / 0 = 0
.
- add : K → K → K
- zero : K
- nsmul : ℕ → K → K
- nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : K → K → K
- one : K
- natCast : ℕ → K
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → K → K
- npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : K → K
- sub : K → K → K
- zsmul : ℤ → K → K
- zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → K
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : K → K
- div : K → K → K
a / b := a * b⁻¹
- zpow : ℤ → K → K
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : K), Field.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : K), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : K), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
- nnratCast : ℚ≥0 → K
- ratCast : ℚ → K
For a nonzero
a
,a⁻¹
is a right multiplicative inverse.The inverse of
0
is0
by convention.However
NNRat.cast
is defined, it must be equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → K → K
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Field.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead. However
Rat.cast q
is defined, it must be propositionally equal toq.num / q.den
.Do not use this lemma directly. Use
Rat.cast_def
instead.- qsmul : ℚ → K → K
- qsmul_def : ∀ (a : ℚ) (x : K), Field.qsmul a x = ↑a * x
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
Rat.cast_def
instead.
Instances
Equations
- Field.toSemifield = Semifield.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯
Equations
- NNRat.smulDivisionSemiring = { smul := DivisionSemiring.nnqsmul }
Alias of NNRat.smul_one_eq_cast
.
Equations
- Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
Alias of Rat.smul_one_eq_cast
.
OfScientific.ofScientific
is the simp-normal form.