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⁻¹ = 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 : NatCast K] [inst : IntCast K] [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 Semiring , Inv , Div , Nontrivial :
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 (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝
  • a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

    zpow_neg' : autoParam (∀ (n : ) (a : α), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹) _auto✝
  • toNontrivial : Nontrivial α
  • 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 Ring , Inv , Div , Nontrivial , RatCast :

    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
      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 CommSemiring , Inv , Div , Nontrivial :
      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 (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝
      • a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹

        zpow_neg' : autoParam (∀ (n : ) (a : α), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹) _auto✝
      • toNontrivial : Nontrivial α
      • 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 CommRing , Inv , Div , Nontrivial , RatCast :

        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 : 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_1} [inst : DivisionRing K] (r : ) :
          r = r.num / r.den
          instance Rat.smulDivisionRing {K : Type u_1} [inst : DivisionRing K] :
          Equations
          • Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
          theorem Rat.smul_def {K : Type u_1} [inst : DivisionRing K] (a : ) (x : K) :
          a x = a * x
          instance Field.toSemifield {K : Type u_1} [inst : Field K] :
          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 : Semiring R] :
          • 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 : Semifield R] :

            Transferring from Semifield to IsField.

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

            Transferring from Field to IsField.

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

            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 : IsField R) :

            Transferring from IsField to Field.

            Equations
            theorem uniq_inv_of_isField (R : Type u) [inst : Ring R] (hf : IsField R) (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.