mathlib3 documentation

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 #

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

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]
@[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]
@[instance]
def semifield.to_comm_semiring (α : Type u_4) [self : semifield α] :
@[instance]
@[instance]
@[class]
structure semifield (α : Type u_4) :
Type u_4

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} [division_ring K] (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} [division_ring K] (r : ) :
r = (r.num) / (r.denom)
@[protected, instance]
Equations
theorem rat.smul_def {K : Type u_3} [division_ring K] (a : ) (x : K) :
a x = a * x
@[simp]
theorem rat.smul_one_eq_coe (A : Type u_1) [division_ring A] (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) :
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.