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

• Rat.castRec q = ↑q.num * (↑q.den)⁻¹

def qsmulRec {K : Type u_3} (coe : ℚ → K) [Mul K] (a : ℚ) (x : K) : K

The default definition of the scalar multiplication by ℚ on a division ring K.

q • x is defined as ↑q * x.

Do not use directly (instances of DivisionRing are allowed to override that default for better definitional properties). Instead use the • notation.

Equations

• qsmulRec coe a x = coe a * x

class DivisionSemiring (α : Type u_4) extends Semiring , Inv , Div , Nontrivial : 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n 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 : α), DivisionSemiring.zpow 0 a = 1

  a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ℕ) (a : α), DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑(Nat.succ n)) 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 ≠ 0 → a * a⁻¹ = 1

  Every nonzero element of a group with zero is invertible.

class DivisionRing (α : Type u_4) extends Ring , Inv , Div , Nontrivial , RatCast : 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : ℤ → α
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.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 : α), DivisionRing.zpow 0 a = 1

  a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑(Nat.succ n)) a)⁻¹

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

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), 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.

• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a * (↑b)⁻¹

  However Rat.cast is defined, it must be propositionally equal to a * b⁻¹.

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

• qsmul : ℚ → α → α

  Scalar multiplication by a rational number.

  Set this to qsmulRec _ unless there is a risk of a Module ℚ _ instance diamond.

  Do not use directly. Instead use the • notation.

• qsmul_eq_mul' : ∀ (a : ℚ) (x : α), 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 DivisionRing.toDivisionSemiring {α : Type u_1} [DivisionRing α] : DivisionSemiring α

Equations

• DivisionRing.toDivisionSemiring = let __src := inst; DivisionSemiring.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯

class Semifield (α : Type u_4) extends CommSemiring , Inv , Div , Nontrivial : 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n 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 : α), Semifield.zpow 0 a = 1

  a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ℕ) (a : α), Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑(Nat.succ n)) 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 ≠ 0 → a * a⁻¹ = 1

  Every nonzero element of a group with zero is invertible.

class Field (K : Type u) extends CommRing , Inv , Div , Nontrivial , RatCast : 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 (Int.ofNat (Nat.succ n)) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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⁻¹

  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 (Nat.succ n)) 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 (↑(Nat.succ n)) a)⁻¹

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

• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• 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.

• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a * (↑b)⁻¹

  However Rat.cast is defined, it must be propositionally equal to a * b⁻¹.

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

• qsmul : ℚ → K → K

  Scalar multiplication by a rational number.

  Set this to qsmulRec _ unless there is a risk of a Module ℚ _ instance diamond.

  Do not use directly. Instead use the • notation.

• qsmul_eq_mul' : ∀ (a : ℚ) (x : K), Field.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 Field.toSemifield {α : Type u_1} [Field α] : Semifield α

Equations

• Field.toSemifield = let __src := inst; Semifield.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯

theorem Rat.cast_mk' {K : Type u_3} [DivisionRing K] (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b) : ↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a * (↑b)⁻¹

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

instance Rat.smulDivisionRing {K : Type u_3} [DivisionRing K] : SMul ℚ K

Equations

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

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

@[simp]

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

instance RatCast.toOfScientific {K : Type u_3} [RatCast K] : OfScientific K

Equations

• RatCast.toOfScientific = { ofScientific := fun (m : ℕ) (b : Bool) (d : ℕ) => ↑(Rat.ofScientific m b d) }