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 #

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 NNRat.castRec {K : Type u_1} [NatCast K] [Div K] (q : ℚ≥0) :
K

The default definition of the coercion ℚ≥0 → K for a division semiring K.

↑q : K is defined as (q.num : K) / (q.den : K).

Do not use this directly (instances of DivisionSemiring are allowed to override that default for better definitional properties). Instead, use the coercion.

Equations
  • q.castRec = q.num / q.den
def Rat.castRec {K : Type u_1} [NatCast K] [IntCast K] [Div 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
  • q.castRec = q.num / q.den
class DivisionSemiring (K : Type u_2) extends Semiring K, GroupWithZero K, NNRatCast K :
Type u_2

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.

Instances
class DivisionRing (K : Type u_2) extends Ring K, DivInvMonoid K, Nontrivial K, NNRatCast K, RatCast K :
Type u_2

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.

Instances
class Semifield (K : Type u_2) extends CommSemiring K, DivisionSemiring K, CommGroupWithZero K :
Type u_2

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.

Instances
class Field (K : Type u) extends CommRing K, DivisionRing K :

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.

Stacks Tag 09FD (first part)

Instances
@[instance 100]
instance Field.toSemifield {K : Type u_1} [Field K] :
Equations
theorem NNRat.cast_def {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) :
q = q.num / q.den
theorem NNRat.smul_def {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (a : K) :
q a = q * a
@[simp]
theorem NNRat.smul_one_eq_cast (K : Type u_1) [DivisionSemiring K] (q : ℚ≥0) :
q 1 = q
@[deprecated NNRat.smul_one_eq_cast (since := "2024-05-03")]
theorem NNRat.smul_one_eq_coe (K : Type u_1) [DivisionSemiring K] (q : ℚ≥0) :
q 1 = q

Alias of NNRat.smul_one_eq_cast.

theorem Rat.cast_def {K : Type u_1} [DivisionRing K] (q : ) :
q = q.num / q.den
theorem Rat.cast_mk' {K : Type u_1} [DivisionRing K] (a : ) (b : ) (h1 : b 0) (h2 : a.natAbs.Coprime b) :
{ num := a, den := b, den_nz := h1, reduced := h2 } = a / b
@[instance 100]
instance Rat.smulDivisionRing {K : Type u_1} [DivisionRing K] :
Equations
theorem Rat.smul_def {K : Type u_1} [DivisionRing K] (a : ) (x : K) :
a x = a * x
@[simp]
theorem Rat.smul_one_eq_cast (A : Type u_2) [DivisionRing A] (m : ) :
m 1 = m
@[deprecated Rat.smul_one_eq_cast (since := "2024-05-03")]
theorem Rat.smul_one_eq_coe (A : Type u_2) [DivisionRing A] (m : ) :
m 1 = m

Alias of Rat.smul_one_eq_cast.