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] : ℚ → K

The default definition of the coercion (↑(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.

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

The default definition of the scalar multiplication (a : ℚ) • (x : K) for a division ring K is given by a • x = (↑ a) * x. Use (a : ℚ) • (x : K) instead of qsmulRec for better definitional behaviour.

class DivisionSemiring (α : Type u_4) extends Semiring , Inv , Div , Nontrivial : Type u_4

• 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 = x + AddMonoid.nsmul n 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 = x * Semiring.npow n 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 = a * DivisionSemiring.zpow (Int.ofNat n) a

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

• 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.

A DivisionSemiring is a Semiring with multiplicative inverses for nonzero elements.

class DivisionRing (K : Type u) extends Ring , Inv , Div , Nontrivial , RatCast : Type u

• 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 = x + AddMonoid.nsmul n 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 = x * Semiring.npow n 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 = a + Ring.zsmul (Int.ofNat n) 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)
• 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), DivisionRing.zpow 0 a = 1

  a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ℕ) (a : K), 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 : ℚ → 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

  We define the inverse of 0 to be 0.

• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹

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

• qsmul : ℚ → K → K

  Multiplication by a rational number.

• qsmul_eq_mul' : ∀ (a : ℚ) (x : K), DivisionRing.qsmul a x = ↑a * x

  However qsmul is defined, propositionally it must be equal to multiplication by ratCast.

A DivisionRing is a Ring with multiplicative inverses for nonzero elements.

An instance of DivisionRing K includes maps ratCast : ℚ → K and qsmul : ℚ → 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].

instance DivisionRing.toDivisionSemiring {α : Type u_1} [DivisionRing α] : DivisionSemiring α

class Semifield (α : Type u_4) extends CommSemiring , Inv , Div , Nontrivial : Type u_4

• 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 = x + AddMonoid.nsmul n 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 = x * Semiring.npow n 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 = a * Semifield.zpow (Int.ofNat n) a

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

• 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.

A Semifield is a CommSemiring with multiplicative inverses for nonzero elements.

class Field (K : Type u) extends CommRing , Inv , Div , Nontrivial , RatCast : Type u

• 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 = x + AddMonoid.nsmul n 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 = x * Semiring.npow n 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 = a + Ring.zsmul (Int.ofNat n) 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 = a * Field.zpow (Int.ofNat n) a

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

• 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 y, 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

  We define the inverse of 0 to be 0.

• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹

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

• qsmul : ℚ → K → K

  Multiplication by a rational number.

• qsmul_eq_mul' : ∀ (a : ℚ) (x : K), Field.qsmul a x = ↑a * x

  However qsmul is defined, propositionally it must be equal to multiplication by ratCast.

A Field is a CommRing with multiplicative inverses for nonzero elements.

An instance of Field K includes maps ratCast : ℚ → K and qsmul : ℚ → 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].

theorem Rat.cast_mk' {K : Type u_3} [DivisionRing K] (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b) : ↑(Rat.mk' a b) = ↑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

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 DivisionRing.toOfScientific {K : Type u_3} [DivisionRing K] : OfScientific K

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