# 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 to Field, 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

def NNRat.castRec {K : Type u_3} [] [Div K] (q : ℚ≥0) :
K

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.

Equations
• q.castRec = q.num / q.den
Instances For
def Rat.castRec {K : Type u_3} [] [] [Div K] (q : ) :
K

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.

Equations
• q.castRec = q.num / q.den
Instances For
class DivisionSemiring (α : Type u_4) extends , , , , :
Type u_4

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 : ααα
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

a / b := a * b⁻¹

• zpow : αα

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α),

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : α), DivisionSemiring.zpow (Int.ofNat n.succ) a = * a

a ^ (n + 1) = a ^ n * a

• zpow_neg' : ∀ (n : ) (a : α), = (DivisionSemiring.zpow (n.succ) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

• nnratCast : ℚ≥0α
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be propositionally equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

• nnqsmul : ℚ≥0αα

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a

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.

Instances
theorem DivisionSemiring.nnratCast_def {α : Type u_4} [self : ] (q : ℚ≥0) :
q = q.num / q.den

However NNRat.cast is defined, it must be propositionally equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

theorem DivisionSemiring.nnqsmul_def {α : Type u_4} [self : ] (q : ℚ≥0) (a : α) :
= q * a

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.

class DivisionRing (α : Type u_4) extends , , , , , :
Type u_4

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 : ααα
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

a / b := a * b⁻¹

• zpow : αα

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α), = 1

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : α), DivisionRing.zpow (Int.ofNat n.succ) a = * a

a ^ (n + 1) = a ^ n * a

• zpow_neg' : ∀ (n : ) (a : α), = (DivisionRing.zpow (n.succ) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

For a nonzero a, a⁻¹ is a right multiplicative inverse.

• inv_zero : 0⁻¹ = 0

The inverse of 0 is 0 by convention.

• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

• nnqsmul : ℚ≥0αα

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a

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.

• ratCast_def : ∀ (q : ), q = q.num / q.den

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.

• qsmul : αα

Scalar multiplication by a rational number.

Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

Do not use directly. Instead use the • notation.

• qsmul_def : ∀ (a : ) (x : α), = a * x

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.

Instances
theorem DivisionRing.mul_inv_cancel {α : Type u_4} [self : ] (a : α) :
a 0a * a⁻¹ = 1

For a nonzero a, a⁻¹ is a right multiplicative inverse.

theorem DivisionRing.inv_zero {α : Type u_4} [self : ] :
0⁻¹ = 0

The inverse of 0 is 0 by convention.

theorem DivisionRing.nnratCast_def {α : Type u_4} [self : ] (q : ℚ≥0) :
q = q.num / q.den

However NNRat.cast is defined, it must be equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

theorem DivisionRing.nnqsmul_def {α : Type u_4} [self : ] (q : ℚ≥0) (a : α) :
= q * a

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.

theorem DivisionRing.ratCast_def {α : Type u_4} [self : ] (q : ) :
q = q.num / q.den

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.

theorem DivisionRing.qsmul_def {α : Type u_4} [self : ] (a : ) (x : α) :
= a * x

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.

@[instance 100]
instance DivisionRing.toDivisionSemiring {α : Type u_1} [] :
Equations
• DivisionRing.toDivisionSemiring = let __src := inst; DivisionSemiring.mk DivisionRing.zpow DivisionRing.nnqsmul
class Semifield (α : Type u_4) extends , , , , :
Type u_4

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 : ααα
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

a / b := a * b⁻¹

• zpow : αα

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α), = 1

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : α), Semifield.zpow (Int.ofNat n.succ) a = * a

a ^ (n + 1) = a ^ n * a

• zpow_neg' : ∀ (n : ) (a : α), = (Semifield.zpow (n.succ) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

• nnratCast : ℚ≥0α
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be propositionally equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

• nnqsmul : ℚ≥0αα

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a

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.

Instances
class Field (K : Type u) extends , , , , , :

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 : KKK
• add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
• zero : K
• zero_add : ∀ (a : K), 0 + a = a
• add_zero : ∀ (a : K), a + 0 = a
• nsmul : KK
• nsmul_zero : ∀ (x : K), = 0
• nsmul_succ : ∀ (n : ) (x : K), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : K), a + b = b + a
• mul : KKK
• left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : K), 0 * a = 0
• mul_zero : ∀ (a : K), a * 0 = 0
• mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
• one : K
• one_mul : ∀ (a : K), 1 * a = a
• mul_one : ∀ (a : K), a * 1 = a
• natCast : K
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : KK
• npow_zero : ∀ (x : K), = 1
• npow_succ : ∀ (n : ) (x : K), Semiring.npow (n + 1) x = * x
• neg : KK
• sub : KKK
• sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
• zsmul : KK
• zsmul_zero' : ∀ (a : K), = 0
• zsmul_succ' : ∀ (n : ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : K), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : K), -a + a = 0
• intCast : K
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• mul_comm : ∀ (a b : K), a * b = b * a
• inv : KK
• div : KKK
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹

a / b := a * b⁻¹

• zpow : KK

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : K), = 1

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : K), Field.zpow (Int.ofNat n.succ) a = Field.zpow () a * a

a ^ (n + 1) = a ^ n * a

• zpow_neg' : ∀ (n : ) (a : K), = (Field.zpow (n.succ) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : K), ∃ (y : K), x y
• nnratCast : ℚ≥0K
• ratCast : K
• mul_inv_cancel : ∀ (a : K), a 0a * a⁻¹ = 1

For a nonzero a, a⁻¹ is a right multiplicative inverse.

• inv_zero : 0⁻¹ = 0

The inverse of 0 is 0 by convention.

• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be equal to a / b.

Do not use this lemma directly. Use NNRat.cast_def instead.

• nnqsmul : ℚ≥0KK

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : K), = q * a

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.

• ratCast_def : ∀ (q : ), q = q.num / q.den

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.

• qsmul : KK

Scalar multiplication by a rational number.

Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

Do not use directly. Instead use the • notation.

• qsmul_def : ∀ (a : ) (x : K), = a * x

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.

Instances
@[instance 100]
instance Field.toSemifield {α : Type u_1} [] :
Equations
• Field.toSemifield = let __src := inst; Semifield.mk Field.zpow Field.nnqsmul
@[instance 100]
instance NNRat.smulDivisionSemiring {α : Type u_1} [] :
Equations
• NNRat.smulDivisionSemiring = { smul := DivisionSemiring.nnqsmul }
theorem NNRat.cast_def {α : Type u_1} [] (q : ℚ≥0) :
q = q.num / q.den
theorem NNRat.smul_def {α : Type u_1} [] (q : ℚ≥0) (a : α) :
q a = q * a
@[simp]
theorem NNRat.smul_one_eq_cast (α : Type u_1) [] (q : ℚ≥0) :
q 1 = q
@[deprecated NNRat.smul_one_eq_cast]
theorem NNRat.smul_one_eq_coe (α : Type u_1) [] (q : ℚ≥0) :
q 1 = q

Alias of NNRat.smul_one_eq_cast.

theorem Rat.cast_def {K : Type u_3} [] (q : ) :
q = q.num / q.den
theorem Rat.cast_mk' {K : Type u_3} [] (a : ) (b : ) (h1 : b 0) (h2 : a.natAbs.Coprime b) :
{ num := a, den := b, den_nz := h1, reduced := h2 } = a / b
@[instance 100]
instance Rat.smulDivisionRing {K : Type u_3} [] :
Equations
• Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
theorem Rat.smul_def {K : Type u_3} [] (a : ) (x : K) :
a x = a * x
@[simp]
theorem Rat.smul_one_eq_cast (A : Type u_4) [] (m : ) :
m 1 = m
@[deprecated Rat.smul_one_eq_cast]
theorem Rat.smul_one_eq_coe (A : Type u_4) [] (m : ) :
m 1 = m

Alias of Rat.smul_one_eq_cast.

@[simp]
theorem Rat.ofScientific_eq_ofScientific (m : ) (s : Bool) (e : ) :
=

OfScientific.ofScientific is the simp-normal form.