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_1} [NatCast K] [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

def Rat.castRec {K : Type u_1} [NatCast K] [IntCast K] [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

class DivisionSemiring (K : Type u_2) extends Semiring K, GroupWithZero K, NNRatCast K : Type u_2

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
• 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 : ℕ → 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
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• 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.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
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' : ∀ (a : K), DivisionSemiring.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : K), DivisionSemiring.zpow (↑n.succ) a = DivisionSemiring.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : K), DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
• nnratCast : ℚ≥0 → K
• 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 → K → K

  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), DivisionSemiring.nnqsmul q 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 (K : Type u_2) extends Ring K, DivInvMonoid K, Nontrivial K, NNRatCast K, RatCast K : Type u_2

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
• 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 : ℕ → 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
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• 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.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
• sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
• zsmul : ℤ → K → K
• zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : K), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : K), -a + a = 0
• 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
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' : ∀ (a : K), DivisionRing.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : K), DivisionRing.zpow (↑n.succ) a = DivisionRing.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : K), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• nnratCast : ℚ≥0 → K
• ratCast : ℚ → K
• mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * 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 → K → K

  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), DivisionRing.nnqsmul q 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 : ℚ → K → K

  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), DivisionRing.qsmul 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 {K : Type u_1} [DivisionRing K] : DivisionSemiring K

Equations

• DivisionRing.toDivisionSemiring = DivisionSemiring.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯

class Semifield (K : Type u_2) extends CommSemiring K, DivisionSemiring K, CommGroupWithZero K : Type u_2

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
• 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 : ℕ → 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
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• 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.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
• mul_comm : ∀ (a b : K), a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' : ∀ (a : K), Semifield.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : K), Semifield.zpow (↑n.succ) a = Semifield.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : K), Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
• nnratCast : ℚ≥0 → K
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Semifield.nnqsmul q a = ↑q * a

class Field (K : Type u) extends CommRing K, DivisionRing K : Type u

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
• 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 : ℕ → 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
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• 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.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
• sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
• zsmul : ℤ → K → K
• zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : K), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : K), -a + a = 0
• intCast : ℤ → K
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm : ∀ (a b : K), a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' : ∀ (a : K), Field.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : K), Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : K), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• nnratCast : ℚ≥0 → K
• ratCast : ℚ → K
• mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Field.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → K → K
• qsmul_def : ∀ (a : ℚ) (x : K), Field.qsmul a x = ↑a * x

@[instance 100]

instance Field.toSemifield {K : Type u_1} [Field K] : Semifield K

Equations

• Field.toSemifield = Semifield.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯

@[instance 100]

instance NNRat.smulDivisionSemiring {K : Type u_1} [DivisionSemiring K] : SMul ℚ≥0 K

Equations

• NNRat.smulDivisionSemiring = { smul := DivisionSemiring.nnqsmul }

theorem NNRat.cast_def {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den

theorem NNRat.smul_def {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (a : K) : q • a = ↑q * a

@[simp]

theorem NNRat.smul_one_eq_cast (K : Type u_1) [DivisionSemiring K] (q : ℚ≥0) : q • 1 = ↑q

@[deprecated NNRat.smul_one_eq_cast]

theorem NNRat.smul_one_eq_coe (K : Type u_1) [DivisionSemiring K] (q : ℚ≥0) : q • 1 = ↑q

Alias of NNRat.smul_one_eq_cast.

theorem Rat.cast_def {K : Type u_1} [DivisionRing K] (q : ℚ) : ↑q = ↑q.num / ↑q.den

theorem Rat.cast_mk' {K : Type u_1} [DivisionRing K] (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_1} [DivisionRing K] : SMul ℚ K

Equations

• Rat.smulDivisionRing = { smul := DivisionRing.qsmul }

theorem Rat.smul_def {K : Type u_1} [DivisionRing K] (a : ℚ) (x : K) : a • x = ↑a * x

@[simp]

theorem Rat.smul_one_eq_cast (A : Type u_2) [DivisionRing A] (m : ℚ) : m • 1 = ↑m

@[deprecated Rat.smul_one_eq_cast]

theorem Rat.smul_one_eq_coe (A : Type u_2) [DivisionRing A] (m : ℚ) : m • 1 = ↑m

Alias of Rat.smul_one_eq_cast.

@[simp]

theorem Rat.ofScientific_eq_ofScientific (m : ℕ) (s : Bool) (e : ℕ) : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e

OfScientific.ofScientific is the simp-normal form.