Documentation

Mathlib.Algebra.Ring.Defs

Semirings and rings #

This file defines semirings, rings and domains. This is analogous to Algebra.Group.Defs and Algebra.Group.Basic, the difference being that the former is about + and * separately, while the present file is about their interaction.

Main definitions #

Tags #

Semiring, CommSemiring, Ring, CommRing, domain, IsDomain, nonzero, units

Previously an import dependency on Mathlib/Algebra/Group/Basic.lean had crept in. In general, the .Defs files in the basic algebraic hierarchy should only depend on earlier .Defs files, without importing .Basic theory development.

These assert_not_exists statements guard against this returning.

Distrib class #

class Distrib (R : Type u_1) extends Mul R, Add R :
Type u_1

A typeclass stating that multiplication is left and right distributive over addition.

  • mul : RRR
  • add : RRR
  • left_distrib (a b c : R) : a * (b + c) = a * b + a * c

    Multiplication is left distributive over addition

  • right_distrib (a b c : R) : (a + b) * c = a * c + b * c

    Multiplication is right distributive over addition

Instances
    class LeftDistribClass (R : Type u_1) [Mul R] [Add R] :

    A typeclass stating that multiplication is left distributive over addition.

    • left_distrib (a b c : R) : a * (b + c) = a * b + a * c

      Multiplication is left distributive over addition

    Instances
      class RightDistribClass (R : Type u_1) [Mul R] [Add R] :

      A typeclass stating that multiplication is right distributive over addition.

      • right_distrib (a b c : R) : (a + b) * c = a * c + b * c

        Multiplication is right distributive over addition

      Instances
        @[instance 100]
        @[instance 100]
        theorem left_distrib {R : Type v} [Mul R] [Add R] [LeftDistribClass R] (a b c : R) :
        a * (b + c) = a * b + a * c
        theorem mul_add {R : Type v} [Mul R] [Add R] [LeftDistribClass R] (a b c : R) :
        a * (b + c) = a * b + a * c

        Alias of left_distrib.

        theorem right_distrib {R : Type v} [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
        (a + b) * c = a * c + b * c
        theorem add_mul {R : Type v} [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
        (a + b) * c = a * c + b * c

        Alias of right_distrib.

        theorem distrib_three_right {R : Type v} [Mul R] [Add R] [RightDistribClass R] (a b c d : R) :
        (a + b + c) * d = a * d + b * d + c * d

        Classes of semirings and rings #

        We make sure that the canonical path from NonAssocSemiring to Ring passes through Semiring, as this is a path which is followed all the time in linear algebra where the defining semilinear map σ : R →+* S depends on the NonAssocSemiring structure of R and S while the module definition depends on the Semiring structure.

        It is not currently possible to adjust priorities by hand (see https://github.com/leanprover/lean4/issues/2115). Instead, the last declared instance is used, so we make sure that Semiring is declared after NonAssocRing, so that Semiring -> NonAssocSemiring is tried before NonAssocRing -> NonAssocSemiring. TODO: clean this once https://github.com/leanprover/lean4/issues/2115 is fixed

        A not-necessarily-unital, not-necessarily-associative semiring. See CommutatorRing and the documentation thereof in case you need a NonUnitalNonAssocSemiring instance on a Lie ring or a Lie algebra.

        Instances

          An associative but not-necessarily unital semiring.

          Instances

            A unital but not-necessarily-associative semiring.

            Instances

              A not-necessarily-unital, not-necessarily-associative ring.

              Instances
                class NonUnitalRing (α : Type u_1) extends NonUnitalNonAssocRing α, NonUnitalSemiring α :
                Type u_1

                An associative but not-necessarily unital ring.

                Instances

                  A unital but not-necessarily-associative ring.

                  Instances
                    class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α :

                    A Semiring is a type with addition, multiplication, a 0 and a 1 where addition is commutative and associative, multiplication is associative and left and right distributive over addition, and 0 and 1 are additive and multiplicative identities.

                    Instances
                      class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R :

                      A Ring is a Semiring with negation making it an additive group.

                      Instances

                        Semirings #

                        theorem add_one_mul {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
                        (a + 1) * b = a * b + b
                        theorem mul_add_one {α : Type u} [Add α] [MulOneClass α] [LeftDistribClass α] (a b : α) :
                        a * (b + 1) = a * b + a
                        theorem one_add_mul {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
                        (1 + a) * b = b + a * b
                        theorem mul_one_add {α : Type u} [Add α] [MulOneClass α] [LeftDistribClass α] (a b : α) :
                        a * (1 + b) = a + a * b
                        theorem two_mul {α : Type u} [NonAssocSemiring α] (n : α) :
                        2 * n = n + n
                        theorem mul_two {α : Type u} [NonAssocSemiring α] (n : α) :
                        n * 2 = n + n
                        theorem ite_zero_mul {α : Type u} [MulZeroClass α] (P : Prop) [Decidable P] (a b : α) :
                        (if P then a else 0) * b = if P then a * b else 0
                        theorem mul_ite_zero {α : Type u} [MulZeroClass α] (P : Prop) [Decidable P] (a b : α) :
                        (a * if P then b else 0) = if P then a * b else 0
                        theorem ite_zero_mul_ite_zero {α : Type u} [MulZeroClass α] (P Q : Prop) [Decidable P] [Decidable Q] (a b : α) :
                        ((if P then a else 0) * if Q then b else 0) = if P Q then a * b else 0
                        theorem mul_boole {α : Type u_1} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
                        (a * if P then 1 else 0) = if P then a else 0
                        theorem boole_mul {α : Type u_1} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
                        (if P then 1 else 0) * a = if P then a else 0

                        A not-necessarily-unital, not-necessarily-associative, but commutative semiring.

                        Instances

                          A non-unital commutative semiring is a NonUnitalSemiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (AddCommMonoid), commutative semigroup (CommSemigroup), distributive laws (Distrib), and multiplication by zero law (MulZeroClass).

                          Instances
                            class CommSemiring (R : Type u) extends Semiring R, CommMonoid R :

                            A commutative semiring is a semiring with commutative multiplication.

                            Instances
                              @[instance 100]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[instance 100]
                              Equations
                              theorem add_mul_self_eq {α : Type u} [CommSemiring α] (a b : α) :
                              (a + b) * (a + b) = a * a + 2 * a * b + b * b
                              theorem add_sq {α : Type u} [CommSemiring α] (a b : α) :
                              (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
                              theorem add_sq' {α : Type u} [CommSemiring α] (a b : α) :
                              (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
                              theorem add_pow_two {α : Type u} [CommSemiring α] (a b : α) :
                              (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

                              Alias of add_sq.

                              class HasDistribNeg (α : Type u_1) [Mul α] extends InvolutiveNeg α :
                              Type u_1

                              Typeclass for a negation operator that distributes across multiplication.

                              This is useful for dealing with submonoids of a ring that contain -1 without having to duplicate lemmas.

                              • neg : αα
                              • neg_neg (x : α) : - -x = x
                              • neg_mul (x y : α) : -x * y = -(x * y)

                                Negation is left distributive over multiplication

                              • mul_neg (x y : α) : x * -y = -(x * y)

                                Negation is right distributive over multiplication

                              Instances
                                @[simp]
                                theorem neg_mul {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                -a * b = -(a * b)
                                @[simp]
                                theorem mul_neg {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                a * -b = -(a * b)
                                theorem neg_mul_neg {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                -a * -b = a * b
                                theorem neg_mul_eq_neg_mul {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                -(a * b) = -a * b
                                theorem neg_mul_eq_mul_neg {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                -(a * b) = a * -b
                                theorem neg_mul_comm {α : Type u} [Mul α] [HasDistribNeg α] (a b : α) :
                                -a * b = a * -b
                                theorem neg_eq_neg_one_mul {α : Type u} [MulOneClass α] [HasDistribNeg α] (a : α) :
                                -a = -1 * a
                                theorem mul_neg_one {α : Type u} [MulOneClass α] [HasDistribNeg α] (a : α) :
                                a * -1 = -a

                                An element of a ring multiplied by the additive inverse of one is the element's additive inverse.

                                theorem neg_one_mul {α : Type u} [MulOneClass α] [HasDistribNeg α] (a : α) :
                                -1 * a = -a

                                The additive inverse of one multiplied by an element of a ring is the element's additive inverse.

                                @[instance 100]
                                Equations

                                Rings #

                                @[instance 100]
                                Equations
                                theorem mul_sub_left_distrib {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
                                a * (b - c) = a * b - a * c
                                theorem mul_sub {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
                                a * (b - c) = a * b - a * c

                                Alias of mul_sub_left_distrib.

                                theorem mul_sub_right_distrib {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
                                (a - b) * c = a * c - b * c
                                theorem sub_mul {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
                                (a - b) * c = a * c - b * c

                                Alias of mul_sub_right_distrib.

                                theorem sub_one_mul {α : Type u} [NonAssocRing α] (a b : α) :
                                (a - 1) * b = a * b - b
                                theorem mul_sub_one {α : Type u} [NonAssocRing α] (a b : α) :
                                a * (b - 1) = a * b - a
                                theorem one_sub_mul {α : Type u} [NonAssocRing α] (a b : α) :
                                (1 - a) * b = b - a * b
                                theorem mul_one_sub {α : Type u} [NonAssocRing α] (a b : α) :
                                a * (1 - b) = a - a * b
                                @[instance 100]
                                instance Ring.toNonUnitalRing {α : Type u} [Ring α] :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[instance 100]
                                instance Ring.toNonAssocRing {α : Type u} [Ring α] :
                                Equations
                                • One or more equations did not get rendered due to their size.

                                A non-unital non-associative commutative ring is a NonUnitalNonAssocRing with commutative multiplication.

                                Instances

                                  A non-unital commutative ring is a NonUnitalRing with commutative multiplication.

                                  Instances
                                    @[instance 100]
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    class CommRing (α : Type u) extends Ring α, CommMonoid α :

                                    A commutative ring is a ring with commutative multiplication.

                                    Instances
                                      @[instance 100]
                                      instance CommRing.toCommSemiring {α : Type u} [s : CommRing α] :
                                      Equations
                                      @[instance 100]
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      @[instance 100]
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α :

                                      A domain is a nontrivial semiring such that multiplication by a non zero element is cancellative on both sides. In other words, a nontrivial semiring R satisfying ∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c.

                                      This is implemented as a mixin for Semiring α. To obtain an integral domain use [CommRing α] [IsDomain α].

                                      Instances