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 Rat.castRec {K : Type u_3} [NatCast K] [IntCast K] [Mul K] [Inv 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
Instances For
    def qsmulRec {K : Type u_3} (coe : K) [Mul K] (a : ) (x : K) :
    K

    The default definition of the scalar multiplication by on a division ring K.

    q • x is defined as ↑q * x.

    Do not use directly (instances of DivisionRing are allowed to override that default for better definitional properties). Instead use the notation.

    Equations
    Instances For
      class DivisionSemiring (α : Type u_4) extends Semiring , Inv , Div , Nontrivial :
      Type u_4

      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 (α : Type u_4) extends Ring , Inv , Div , Nontrivial , RatCast :
        Type u_4

        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
          Equations
          • DivisionRing.toDivisionSemiring = let __src := inst; DivisionSemiring.mk DivisionRing.zpow
          class Semifield (α : Type u_4) extends CommSemiring , Inv , Div , Nontrivial :
          Type u_4

          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.

          • 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 : α), AddMonoid.nsmul 0 x = 0
          • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
          • 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
          • natCast : α
          • natCast_zero : NatCast.natCast 0 = 0
          • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
          • npow : αα
          • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
          • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n x
          • mul_comm : ∀ (a b : α), a * b = b * a
          • inv : αα
          • div : ααα
          • div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

            a / b := a * b⁻¹

          • zpow : αα

            The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

          • zpow_zero' : ∀ (a : α), Semifield.zpow 0 a = 1

            a ^ 0 = 1

          • zpow_succ' : ∀ (n : ) (a : α), Semifield.zpow (Int.ofNat (Nat.succ n)) a = a * Semifield.zpow (Int.ofNat n) a

            a ^ (n + 1) = a * a ^ n

          • zpow_neg' : ∀ (n : ) (a : α), Semifield.zpow (Int.negSucc n) a = (Semifield.zpow ((Nat.succ n)) a)⁻¹

            a ^ -(n + 1) = (a ^ (n + 1))⁻¹

          • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
          • inv_zero : 0⁻¹ = 0

            The inverse of 0 in a group with zero is 0.

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

            Every nonzero element of a group with zero is invertible.

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

            Instances
              instance Field.toSemifield {α : Type u_1} [Field α] :
              Equations
              • Field.toSemifield = let __src := inst; Semifield.mk Field.zpow
              theorem Rat.cast_mk' {K : Type u_3} [DivisionRing K] (a : ) (b : ) (h1 : b 0) (h2 : Nat.Coprime (Int.natAbs a) b) :
              { num := a, den := b, den_nz := h1, reduced := h2 } = a * (b)⁻¹
              theorem Rat.cast_def {K : Type u_3} [DivisionRing K] (r : ) :
              r = r.num / r.den
              instance Rat.smulDivisionRing {K : Type u_3} [DivisionRing K] :
              Equations
              • Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
              theorem Rat.smul_def {K : Type u_3} [DivisionRing K] (a : ) (x : K) :
              a x = a * x
              @[simp]
              theorem Rat.smul_one_eq_coe (A : Type u_4) [DivisionRing A] (m : ) :
              m 1 = m
              Equations