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
Instances For
    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
    Instances For
      class DivisionSemiring (K : Type u_2) extends Semiring , Inv , Div , Nontrivial , NNRatCast :
      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
        theorem DivisionSemiring.nnratCast_def {K : Type u_2} [self : DivisionSemiring K] (q : ℚ≥0) :
        q = q.num / q.den

        However NNRat.cast is defined, it must be propositionally equal to a / b.

        Do not use this lemma directly. Use NNRat.cast_def instead.

        theorem DivisionSemiring.nnqsmul_def {K : Type u_2} [self : DivisionSemiring K] (q : ℚ≥0) (a : K) :

        However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

        Do not use this lemma directly. Use NNRat.smul_def instead.

        class DivisionRing (K : Type u_2) extends Ring , Inv , Div , Nontrivial , NNRatCast , RatCast :
        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.

        • add : KKK
        • add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
        • zero : K
        • zero_add : ∀ (a : K), 0 + a = a
        • add_zero : ∀ (a : K), a + 0 = a
        • nsmul : KK
        • nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
        • nsmul_succ : ∀ (n : ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
        • add_comm : ∀ (a b : K), a + b = b + a
        • mul : KKK
        • left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c
        • right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
        • zero_mul : ∀ (a : K), 0 * a = 0
        • mul_zero : ∀ (a : K), a * 0 = 0
        • mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
        • one : K
        • one_mul : ∀ (a : K), 1 * a = a
        • mul_one : ∀ (a : K), a * 1 = a
        • natCast : K
        • natCast_zero : NatCast.natCast 0 = 0
        • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
        • npow : KK
        • npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
        • npow_succ : ∀ (n : ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
        • neg : KK
        • sub : KKK
        • sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
        • zsmul : KK
        • zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
        • zsmul_succ' : ∀ (n : ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
        • zsmul_neg' : ∀ (n : ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
        • neg_add_cancel : ∀ (a : K), -a + a = 0
        • intCast : K
        • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
        • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
        • inv : KK
        • div : KKK
        • div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹

          a / b := a * b⁻¹

        • zpow : KK

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

        • zpow_zero' : ∀ (a : K), DivisionRing.zpow 0 a = 1

          a ^ 0 = 1

        • zpow_succ' : ∀ (n : ) (a : K), DivisionRing.zpow (Int.ofNat n.succ) a = DivisionRing.zpow (Int.ofNat n) a * a

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

        • zpow_neg' : ∀ (n : ) (a : K), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹

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

        • exists_pair_ne : ∃ (x : K), ∃ (y : K), x y
        • nnratCast : ℚ≥0K
        • ratCast : K
        • mul_inv_cancel : ∀ (a : K), a 0a * a⁻¹ = 1

          For a nonzero a, a⁻¹ is a right multiplicative inverse.

        • inv_zero : 0⁻¹ = 0

          The inverse of 0 is 0 by convention.

        • nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

          However NNRat.cast is defined, it must be equal to a / b.

          Do not use this lemma directly. Use NNRat.cast_def instead.

        • nnqsmul : ℚ≥0KK

          Scalar multiplication by a nonnegative rational number.

          Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

          Do not use directly. Instead use the notation.

        • nnqsmul_def : ∀ (q : ℚ≥0) (a : K), DivisionRing.nnqsmul q a = q * a

          However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

          Do not use this lemma directly. Use NNRat.smul_def instead.

        • ratCast_def : ∀ (q : ), q = q.num / q.den

          However Rat.cast q is defined, it must be propositionally equal to q.num / q.den.

          Do not use this lemma directly. Use Rat.cast_def instead.

        • qsmul : KK

          Scalar multiplication by a rational number.

          Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

          Do not use directly. Instead use the notation.

        • qsmul_def : ∀ (a : ) (x : K), DivisionRing.qsmul a x = a * x

          However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

          Do not use this lemma directly. Use Rat.cast_def instead.

        Instances
          theorem DivisionRing.mul_inv_cancel {K : Type u_2} [self : DivisionRing K] (a : K) :
          a 0a * a⁻¹ = 1

          For a nonzero a, a⁻¹ is a right multiplicative inverse.

          theorem DivisionRing.inv_zero {K : Type u_2} [self : DivisionRing K] :
          0⁻¹ = 0

          The inverse of 0 is 0 by convention.

          theorem DivisionRing.nnratCast_def {K : Type u_2} [self : DivisionRing K] (q : ℚ≥0) :
          q = q.num / q.den

          However NNRat.cast is defined, it must be equal to a / b.

          Do not use this lemma directly. Use NNRat.cast_def instead.

          theorem DivisionRing.nnqsmul_def {K : Type u_2} [self : DivisionRing K] (q : ℚ≥0) (a : K) :

          However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

          Do not use this lemma directly. Use NNRat.smul_def instead.

          theorem DivisionRing.ratCast_def {K : Type u_2} [self : DivisionRing K] (q : ) :
          q = q.num / q.den

          However Rat.cast q is defined, it must be propositionally equal to q.num / q.den.

          Do not use this lemma directly. Use Rat.cast_def instead.

          theorem DivisionRing.qsmul_def {K : Type u_2} [self : DivisionRing K] (a : ) (x : K) :

          However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

          Do not use this lemma directly. Use Rat.cast_def instead.

          @[instance 100]
          Equations
          • DivisionRing.toDivisionSemiring = DivisionSemiring.mk DivisionRing.zpow DivisionRing.nnqsmul
          class Semifield (K : Type u_2) extends CommSemiring , Inv , Div , Nontrivial , NNRatCast :
          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.

          • add : KKK
          • add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
          • zero : K
          • zero_add : ∀ (a : K), 0 + a = a
          • add_zero : ∀ (a : K), a + 0 = a
          • nsmul : KK
          • nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
          • nsmul_succ : ∀ (n : ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
          • add_comm : ∀ (a b : K), a + b = b + a
          • mul : KKK
          • left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c
          • right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
          • zero_mul : ∀ (a : K), 0 * a = 0
          • mul_zero : ∀ (a : K), a * 0 = 0
          • mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
          • one : K
          • one_mul : ∀ (a : K), 1 * a = a
          • mul_one : ∀ (a : K), a * 1 = a
          • natCast : K
          • natCast_zero : NatCast.natCast 0 = 0
          • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
          • npow : KK
          • npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
          • npow_succ : ∀ (n : ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
          • mul_comm : ∀ (a b : K), a * b = b * a
          • inv : KK
          • div : KKK
          • div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹

            a / b := a * b⁻¹

          • zpow : KK

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

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

            a ^ 0 = 1

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

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

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

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

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

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

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

            Every nonzero element of a group with zero is invertible.

          • nnratCast : ℚ≥0K
          • nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

            However NNRat.cast is defined, it must be propositionally equal to a / b.

            Do not use this lemma directly. Use NNRat.cast_def instead.

          • nnqsmul : ℚ≥0KK

            Scalar multiplication by a nonnegative rational number.

            Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

            Do not use directly. Instead use the notation.

          • nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Semifield.nnqsmul q a = q * a

            However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

            Do not use this lemma directly. Use NNRat.smul_def instead.

          Instances
            class Field (K : Type u) extends CommRing , Inv , Div , Nontrivial , NNRatCast , 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.

            • add : KKK
            • add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
            • zero : K
            • zero_add : ∀ (a : K), 0 + a = a
            • add_zero : ∀ (a : K), a + 0 = a
            • nsmul : KK
            • nsmul_zero : ∀ (x : K), AddMonoid.nsmul 0 x = 0
            • nsmul_succ : ∀ (n : ) (x : K), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
            • add_comm : ∀ (a b : K), a + b = b + a
            • mul : KKK
            • left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c
            • right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
            • zero_mul : ∀ (a : K), 0 * a = 0
            • mul_zero : ∀ (a : K), a * 0 = 0
            • mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
            • one : K
            • one_mul : ∀ (a : K), 1 * a = a
            • mul_one : ∀ (a : K), a * 1 = a
            • natCast : K
            • natCast_zero : NatCast.natCast 0 = 0
            • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
            • npow : KK
            • npow_zero : ∀ (x : K), Semiring.npow 0 x = 1
            • npow_succ : ∀ (n : ) (x : K), Semiring.npow (n + 1) x = Semiring.npow n x * x
            • neg : KK
            • sub : KKK
            • sub_eq_add_neg : ∀ (a b : K), a - b = a + -b
            • zsmul : KK
            • zsmul_zero' : ∀ (a : K), Ring.zsmul 0 a = 0
            • zsmul_succ' : ∀ (n : ) (a : K), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
            • zsmul_neg' : ∀ (n : ) (a : K), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
            • neg_add_cancel : ∀ (a : K), -a + a = 0
            • intCast : K
            • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
            • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
            • mul_comm : ∀ (a b : K), a * b = b * a
            • inv : KK
            • div : KKK
            • div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹

              a / b := a * b⁻¹

            • zpow : KK

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

            • zpow_zero' : ∀ (a : K), Field.zpow 0 a = 1

              a ^ 0 = 1

            • zpow_succ' : ∀ (n : ) (a : K), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a

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

            • zpow_neg' : ∀ (n : ) (a : K), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹

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

            • exists_pair_ne : ∃ (x : K), ∃ (y : K), x y
            • nnratCast : ℚ≥0K
            • ratCast : K
            • mul_inv_cancel : ∀ (a : K), a 0a * a⁻¹ = 1

              For a nonzero a, a⁻¹ is a right multiplicative inverse.

            • inv_zero : 0⁻¹ = 0

              The inverse of 0 is 0 by convention.

            • nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

              However NNRat.cast is defined, it must be equal to a / b.

              Do not use this lemma directly. Use NNRat.cast_def instead.

            • nnqsmul : ℚ≥0KK

              Scalar multiplication by a nonnegative rational number.

              Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

              Do not use directly. Instead use the notation.

            • nnqsmul_def : ∀ (q : ℚ≥0) (a : K), Field.nnqsmul q a = q * a

              However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

              Do not use this lemma directly. Use NNRat.smul_def instead.

            • ratCast_def : ∀ (q : ), q = q.num / q.den

              However Rat.cast q is defined, it must be propositionally equal to q.num / q.den.

              Do not use this lemma directly. Use Rat.cast_def instead.

            • qsmul : KK

              Scalar multiplication by a rational number.

              Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

              Do not use directly. Instead use the notation.

            • qsmul_def : ∀ (a : ) (x : K), Field.qsmul a x = a * x

              However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

              Do not use this lemma directly. Use Rat.cast_def instead.

            Instances
              @[instance 100]
              instance Field.toSemifield {K : Type u_1} [Field K] :
              Equations
              • Field.toSemifield = Semifield.mk Field.zpow Field.nnqsmul
              @[instance 100]
              Equations
              • NNRat.smulDivisionSemiring = { smul := DivisionSemiring.nnqsmul }
              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]
              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
              • Rat.smulDivisionRing = { smul := DivisionRing.qsmul }
              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]
              theorem Rat.smul_one_eq_coe (A : Type u_2) [DivisionRing A] (m : ) :
              m 1 = m

              Alias of Rat.smul_one_eq_cast.