# Documentation

Mathlib.Algebra.Field.Defs

# 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⁻¹ = 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≠ 0 when writing x⁻¹⁻¹. With this convention in place, some statements like (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹⁻¹ = a * c⁻¹ + b * c⁻¹⁻¹ + b * c⁻¹⁻¹ still remain true, while others like the defining property a * a⁻¹ = 1⁻¹ = 1 need the assumption a ≠ 0≠ 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_1} [inst : ] [inst : ] [inst : Mul K] [inst : Inv K] :
K

The default definition of the coercion (↑(a : ℚ) : K)↑(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.

Equations
def qsmulRec {K : Type u_1} (coe : K) [inst : 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↑ a) * x. Use (a : ℚ) • (x : K) instead of qsmulRec for better definitional behaviour.

Equations
class DivisionSemiring (α : Type u_1) extends , , , :
Type u_1
• The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹ (n times)

zpow : αα
• a ^ 0 = 1

zpow_zero' : autoParam (∀ (a : α), zpow 0 a = 1) _auto✝
• a ^ (n + 1) = a * a ^ n

zpow_succ' : autoParam (∀ (n : ) (a : α), zpow () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : α), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• toNontrivial :
• The inverse of 0 in a group with zero is 0.

inv_zero : 0⁻¹ = 0
• Every nonzero element of a group with zero is invertible.

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

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

Instances
class DivisionRing (K : Type u) extends , , , , :
• a ^ 0 = 1

zpow_zero' : autoParam (∀ (a : K), zpow 0 a = 1) _auto✝
• a ^ (n + 1) = a * a ^ n

zpow_succ' : autoParam (∀ (n : ) (a : K), zpow () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : K), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• toNontrivial :
• toRatCast :
• For a nonzero a, a⁻¹⁻¹ is a right multiplicative inverse.

mul_inv_cancel : ∀ (a : K), a 0a * a⁻¹ = 1
• We define the inverse of 0 to be 0.

inv_zero : 0⁻¹ = 0
• However ratCast is defined, propositionally it must be equal to a * b⁻¹⁻¹.

ratCast_mk : autoParam (∀ (a : ) (b : ) (h1 : b 0) (h2 : ), ↑(Rat.mk' a b) = a * (b)⁻¹) _auto✝
• Multiplication by a rational number.

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

qsmul_eq_mul' : autoParam (∀ (a : ) (x : K), qsmul a x = a * x) _auto✝

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

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

Instances
instance DivisionRing.toDivisionSemiring {α : Type u_1} [inst : ] :
Equations
• DivisionRing.toDivisionSemiring = let src := inst; let src_1 := inferInstance; DivisionSemiring.mk DivisionRing.zpow (_ : 0⁻¹ = 0) (_ : ∀ (a : α), a 0a * a⁻¹ = 1)
class Semifield (α : Type u_1) extends , , , :
Type u_1
• The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹ (n times)

zpow : αα
• a ^ 0 = 1

zpow_zero' : autoParam (∀ (a : α), zpow 0 a = 1) _auto✝
• a ^ (n + 1) = a * a ^ n

zpow_succ' : autoParam (∀ (n : ) (a : α), zpow () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : α), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• toNontrivial :
• The inverse of 0 in a group with zero is 0.

inv_zero : 0⁻¹ = 0
• Every nonzero element of a group with zero is invertible.

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

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

Instances
class Field (K : Type u) extends , , , , :
• a ^ 0 = 1

zpow_zero' : autoParam (∀ (a : K), zpow 0 a = 1) _auto✝
• a ^ (n + 1) = a * a ^ n

zpow_succ' : autoParam (∀ (n : ) (a : K), zpow () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : K), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• toNontrivial :
• toRatCast :
• For a nonzero a, a⁻¹⁻¹ is a right multiplicative inverse.

mul_inv_cancel : ∀ (a : K), a 0a * a⁻¹ = 1
• We define the inverse of 0 to be 0.

inv_zero : 0⁻¹ = 0
• However ratCast is defined, propositionally it must be equal to a * b⁻¹⁻¹.

ratCast_mk : autoParam (∀ (a : ) (b : ) (h1 : b 0) (h2 : ), ↑(Rat.mk' a b) = a * (b)⁻¹) _auto✝
• Multiplication by a rational number.

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

qsmul_eq_mul' : autoParam (∀ (a : ) (x : K), qsmul a x = a * x) _auto✝

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

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

Instances
theorem Rat.cast_mk' {K : Type u_1} [inst : ] (a : ) (b : ) (h1 : b 0) (h2 : ) :
↑(Rat.mk' a b) = a * (b)⁻¹
theorem Rat.cast_def {K : Type u_1} [inst : ] (r : ) :
r = r.num / r.den
instance Rat.smulDivisionRing {K : Type u_1} [inst : ] :
Equations
• Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
theorem Rat.smul_def {K : Type u_1} [inst : ] (a : ) (x : K) :
a x = a * x
instance Field.toSemifield {K : Type u_1} [inst : ] :
Equations
• Field.toSemifield = let src := inst; let src_1 := inferInstance; Semifield.mk Field.zpow (_ : 0⁻¹ = 0) (_ : ∀ (a : K), a 0a * a⁻¹ = 1)
structure IsField (R : Type u) [inst : ] :
• For a semiring to be a field, it must have two distinct elements.

exists_pair_ne : x y, x y
• Fields are commutative.

mul_comm : ∀ (x y : R), x * y = y * x
• Nonzero elements have multiplicative inverses.

mul_inv_cancel : ∀ {a : R}, a 0b, a * b = 1

A predicate to express that a (semi)ring is a (semi)field.

This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms. Additionaly, this is useful when trying to prove that a particular ring structure extends to a (semi)field.

Instances For
theorem Semifield.toIsField (R : Type u) [inst : ] :

Transferring from Semifield to IsField.

theorem Field.toIsField (R : Type u) [inst : ] :

Transferring from Field to IsField.

@[simp]
theorem IsField.nontrivial {R : Type u} [inst : ] (h : ) :
@[simp]
theorem not_isField_of_subsingleton (R : Type u) [inst : ] [inst : ] :
noncomputable def IsField.toSemifield {R : Type u} [inst : ] (h : ) :

Transferring from IsField to Semifield.

Equations
• One or more equations did not get rendered due to their size.
noncomputable def IsField.toField {R : Type u} [inst : Ring R] (h : ) :

Transferring from IsField to Field.

Equations
theorem uniq_inv_of_isField (R : Type u) [inst : Ring R] (hf : ) (x : R) :
x 0∃! y, x * y = 1

For each field, and for each nonzero element of said field, there is a unique inverse. Since IsField doesn't remember the data of an inv function and as such, a lemma that there is a unique inverse could be useful.