# mathlib3documentation

algebra.field.defs

# Division (semi)rings and (semi)fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 field_theory folder.

## Main definitions #

• division_semiring: Nontrivial semiring with multiplicative inverses for nonzero elements.
• division_ring: : Nontrivial ring with multiplicative inverses for nonzero elements.
• semifield: Commutative division semiring.
• field: Commutative division ring.
• is_field: 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 group_with_zero. If you cannot find a division ring / field lemma that does not involve +, you can try looking for a group_with_zero lemma instead.

## Tags #

field, division ring, skew field, skew-field, skewfield

def rat.cast_rec {K : Type u_3} [ K] [ K] [has_mul K] [has_inv 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.cast_rec for better definitional behaviour.

Equations
@[class]
structure has_rat_cast (K : Type u) :

Type class for the canonical homomorphism ℚ → K.

Instances of this typeclass
Instances of other typeclasses for has_rat_cast
• has_rat_cast.has_sizeof_inst
def qsmul_rec {K : Type u_3} (coe : K) [has_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 qsmul_rec for better definitional behaviour.

Equations
@[class]
structure division_semiring (α : Type u_4) :
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 : α), = 0) . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), = x + . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), = 1) . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), = x * . "try_refl_tac"
• inv : α α
• div : α α α
• div_eq_mul_inv : ( (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : α α
• zpow_zero' : ( (a : α), = 1) . "try_refl_tac"
• zpow_succ' : ( (n : ) (a : α), = a * . "try_refl_tac"
• zpow_neg' : ( (n : ) (a : α), = a)⁻¹) . "try_refl_tac"
• exists_pair_ne : (x y : α), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : (a : α), a 0 a * a⁻¹ = 1

A division_semiring is a semiring with multiplicative inverses for nonzero elements.

Instances of this typeclass
Instances of other typeclasses for division_semiring
• division_semiring.has_sizeof_inst
@[instance]
@[instance]
def division_semiring.to_semiring (α : Type u_4) [self : division_semiring α] :
@[instance]
def division_ring.to_nontrivial (K : Type u) [self : division_ring K] :
@[instance]
@[class]
structure division_ring (K : Type u) :

A division_ring is a ring with multiplicative inverses for nonzero elements.

An instance of division_ring K includes maps rat_cast : ℚ → K and qsmul : ℚ → K → K. If the division ring has positive characteristic p, we define rat_cast (1 / p) = 1 / 0 = 0 for consistency with our division by zero convention. The fields rat_cast and qsmul are needed to implement the algebra_rat [division_ring 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 of this typeclass
Instances of other typeclasses for division_ring
• division_ring.has_sizeof_inst
@[instance]
def division_ring.to_ring (K : Type u) [self : division_ring K] :
@[instance]
@[protected, instance]
Equations
@[instance]
def semifield.to_comm_semiring (α : Type u_4) [self : semifield α] :
@[instance]
def semifield.to_comm_group_with_zero (α : Type u_4) [self : semifield α] :
@[instance]
def semifield.to_division_semiring (α : Type u_4) [self : semifield α] :
@[class]
structure semifield (α : Type u_4) :
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 : α), = 0) . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), = x + x) . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), semifield.nat_cast (n + 1) = . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), = 1) . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), = x * x) . "try_refl_tac"
• mul_comm : (a b : α), a * b = b * a
• inv : α α
• div : α α α
• div_eq_mul_inv : ( (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : α α
• zpow_zero' : ( (a : α), = 1) . "try_refl_tac"
• zpow_succ' : ( (n : ) (a : α), a = a * a) . "try_refl_tac"
• zpow_neg' : ( (n : ) (a : α), = (semifield.zpow (n.succ) a)⁻¹) . "try_refl_tac"
• exists_pair_ne : (x y : α), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : (a : α), a 0 a * a⁻¹ = 1

A semifield is a comm_semiring with multiplicative inverses for nonzero elements.

Instances of this typeclass
Instances of other typeclasses for semifield
• semifield.has_sizeof_inst
@[instance]
def field.to_comm_ring (K : Type u) [self : field K] :
@[instance]
def field.to_division_ring (K : Type u) [self : field K] :
@[class]
structure field (K : Type u) :

A field is a comm_ring with multiplicative inverses for nonzero elements.

An instance of field K includes maps of_rat : ℚ → K and qsmul : ℚ → K → K. If the field has positive characteristic p, we define of_rat (1 / p) = 1 / 0 = 0 for consistency with our division by zero convention. The fields of_rat and qsmul are needed to implement thealgebra_rat [division_ring K] : algebra ℚ Kinstance, since we need to control the specific definitions for some special cases ofK(in particularK = ℚ itself). See also Note [forgetful inheritance].

Instances of this typeclass
Instances of other typeclasses for field
• field.has_sizeof_inst
@[protected, instance]
def rat.cast_coe {K : Type u_1} [has_rat_cast K] :

Construct the canonical injection from ℚ into an arbitrary division ring. If the field has positive characteristic p, we define 1 / p = 1 / 0 = 0 for consistency with our division by zero convention.

Equations
theorem rat.cast_mk' {K : Type u_3} (a : ) (b : ) (h1 : 0 < b) (h2 : a.nat_abs.coprime b) :
{num := a, denom := b, pos := h1, cop := h2} = a * (b)⁻¹
theorem rat.cast_def {K : Type u_3} (r : ) :
r = (r.num) / (r.denom)
@[protected, instance]
def rat.smul_division_ring {K : Type u_3}  :
Equations
theorem rat.smul_def {K : Type u_3} (a : ) (x : K) :
a x = a * x
@[simp]
theorem rat.smul_one_eq_coe (A : Type u_1) (m : ) :
m 1 = m
@[protected, instance]
def field.to_semifield {K : Type u_3} [field K] :
Equations
structure is_field (R : Type u) [semiring R] :
Prop
• exists_pair_ne : (x y : R), x y
• mul_comm : (x y : R), x * y = y * x
• mul_inv_cancel : {a : R}, a 0 ( (b : R), 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.

theorem semifield.to_is_field (R : Type u) [semifield R] :

Transferring from semifield to is_field.

theorem field.to_is_field (R : Type u) [field R] :

Transferring from field to is_field.

@[simp]
theorem is_field.nontrivial {R : Type u} [semiring R] (h : is_field R) :
@[simp]
noncomputable def is_field.to_semifield {R : Type u} [semiring R] (h : is_field R) :

Transferring from is_field to semifield.

Equations
noncomputable def is_field.to_field {R : Type u} [ring R] (h : is_field R) :

Transferring from is_field to field.

Equations
theorem uniq_inv_of_is_field (R : Type u) [ring R] (hf : is_field R) (x : R) :
x 0 (∃! (y : R), x * y = 1)

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