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

Distrib class #

class Distrib (R : Type u_1) extends Mul , Add :
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
    theorem Distrib.left_distrib {R : Type u_1} [self : Distrib R] (a : R) (b : R) (c : R) :
    a * (b + c) = a * b + a * c

    Multiplication is left distributive over addition

    theorem Distrib.right_distrib {R : Type u_1} [self : Distrib R] (a : R) (b : R) (c : R) :
    (a + b) * c = a * c + b * c

    Multiplication is right distributive over addition

    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
      theorem LeftDistribClass.left_distrib {R : Type u_1} [Mul R] [Add R] [self : LeftDistribClass R] (a : R) (b : R) (c : R) :
      a * (b + c) = a * b + a * c

      Multiplication is left distributive over addition

      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
        theorem RightDistribClass.right_distrib {R : Type u_1} [Mul R] [Add R] [self : RightDistribClass R] (a : R) (b : R) (c : R) :
        (a + b) * c = a * c + b * c

        Multiplication is right distributive over addition

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

        Alias of left_distrib.

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

        Alias of right_distrib.

        theorem distrib_three_right {R : Type x} [Mul R] [Add R] [RightDistribClass R] (a : R) (b : R) (c : R) (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 lean4#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 lean4#2115 is fixed

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

        • 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 = AddMonoid.nsmul n x + x
        • add_comm : ∀ (a b : α), a + b = b + a
        • mul : ααα
        • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c

          Multiplication is left distributive over addition

        • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

          Multiplication is right distributive over addition

        • zero_mul : ∀ (a : α), 0 * a = 0

          Zero is a left absorbing element for multiplication

        • mul_zero : ∀ (a : α), a * 0 = 0

          Zero is a right absorbing element for multiplication

        Instances

          An associative but not-necessarily unital semiring.

          • 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 = AddMonoid.nsmul n x + 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)

            Multiplication is associative

          Instances

            A unital but not-necessarily-associative semiring.

            • 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 = AddMonoid.nsmul n x + 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
            • one : α
            • one_mul : ∀ (a : α), 1 * a = a

              One is a left neutral element for multiplication

            • mul_one : ∀ (a : α), a * 1 = a

              One is a right neutral element for multiplication

            • natCast : α
            • natCast_zero : NatCast.natCast 0 = 0

              The canonical map ℕ → R sends 0 : ℕ to 0 : R.

            • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1

              The canonical map ℕ → R is a homomorphism.

            Instances
              class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup , Mul :

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

              • 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 = AddMonoid.nsmul n x + x
              • neg : αα
              • sub : ααα
              • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
              • zsmul : αα
              • zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
              • zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
              • zsmul_neg' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (n.succ) a
              • add_left_neg : ∀ (a : α), -a + a = 0
              • add_comm : ∀ (a b : α), a + b = b + a
              • mul : ααα
              • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c

                Multiplication is left distributive over addition

              • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

                Multiplication is right distributive over addition

              • zero_mul : ∀ (a : α), 0 * a = 0

                Zero is a left absorbing element for multiplication

              • mul_zero : ∀ (a : α), a * 0 = 0

                Zero is a right absorbing element for multiplication

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

                An associative but not-necessarily unital ring.

                Instances
                  class NonAssocRing (α : Type u_1) extends NonUnitalNonAssocRing , One , NatCast , IntCast :
                  Type u_1

                  A unital but not-necessarily-associative ring.

                  • 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 = AddMonoid.nsmul n x + x
                  • neg : αα
                  • sub : ααα
                  • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
                  • zsmul : αα
                  • zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
                  • zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
                  • zsmul_neg' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (n.succ) a
                  • add_left_neg : ∀ (a : α), -a + a = 0
                  • 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
                  • one : α
                  • one_mul : ∀ (a : α), 1 * a = a

                    One is a left neutral element for multiplication

                  • mul_one : ∀ (a : α), a * 1 = a

                    One is a right neutral element for multiplication

                  • natCast : α
                  • natCast_zero : NatCast.natCast 0 = 0

                    The canonical map ℕ → R sends 0 : ℕ to 0 : R.

                  • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1

                    The canonical map ℕ → R is a homomorphism.

                  • intCast : α
                  • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n

                    The canonical homomorphism ℤ → R agrees with the one from ℕ → R on .

                  • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)

                    The canonical homomorphism ℤ → R for negative values is just the negation of the values of the canonical homomorphism ℕ → R.

                  Instances
                    class Semiring (α : Type u) extends NonUnitalSemiring , One , NatCast :

                    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.

                    • 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 = AddMonoid.nsmul n x + 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

                      One is a left neutral element for multiplication

                    • mul_one : ∀ (a : α), a * 1 = a

                      One is a right neutral element for multiplication

                    • natCast : α
                    • natCast_zero : NatCast.natCast 0 = 0

                      The canonical map ℕ → R sends 0 : ℕ to 0 : R.

                    • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1

                      The canonical map ℕ → R is a homomorphism.

                    • npow : αα

                      Raising to the power of a natural number.

                    • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1

                      Raising to the power (0 : ℕ) gives 1.

                    • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x

                      Raising to the power (n + 1 : ℕ) behaves as expected.

                    Instances
                      class Ring (R : Type u) extends Semiring , Neg , Sub , IntCast :

                      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 bit0_eq_two_mul {α : Type u} [NonAssocSemiring α] (n : α) :
                        bit0 n = 2 * n
                        theorem mul_two {α : Type u} [NonAssocSemiring α] (n : α) :
                        n * 2 = n + n
                        theorem add_ite {α : Type u_1} [Add α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) :
                        (a + if P then b else c) = if P then a + b else a + c
                        @[simp]
                        theorem mul_ite {α : Type u_1} [Mul α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) :
                        (a * if P then b else c) = if P then a * b else a * c
                        theorem ite_add {α : Type u_1} [Add α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) :
                        (if P then a else b) + c = if P then a + c else b + c
                        @[simp]
                        theorem ite_mul {α : Type u_1} [Mul α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) :
                        (if P then a else b) * c = if P then a * c else b * c
                        theorem ite_sub_ite {α : Type u_1} [Sub α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) (d : α) :
                        ((if P then a else b) - if P then c else d) = if P then a - c else b - d
                        theorem ite_add_ite {α : Type u_1} [Add α] (P : Prop) [Decidable P] (a : α) (b : α) (c : α) (d : α) :
                        ((if P then a else b) + if P then c else d) = if P then a + c else b + d
                        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 : Prop) (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.

                        • 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 = AddMonoid.nsmul n x + 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_comm : ∀ (a b : α), a * b = b * a

                          Multiplication is commutative in a commutative multiplicative magma.

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

                          • 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 = AddMonoid.nsmul n x + 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)
                          • mul_comm : ∀ (a b : α), a * b = b * a

                            Multiplication is commutative in a commutative multiplicative magma.

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

                            A commutative semiring is a semiring with commutative multiplication.

                            • add : RRR
                            • add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
                            • zero : R
                            • zero_add : ∀ (a : R), 0 + a = a
                            • add_zero : ∀ (a : R), a + 0 = a
                            • nsmul : RR
                            • nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
                            • nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
                            • add_comm : ∀ (a b : R), a + b = b + a
                            • mul : RRR
                            • left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
                            • right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
                            • zero_mul : ∀ (a : R), 0 * a = 0
                            • mul_zero : ∀ (a : R), a * 0 = 0
                            • mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
                            • one : R
                            • one_mul : ∀ (a : R), 1 * a = a
                            • mul_one : ∀ (a : R), a * 1 = a
                            • natCast : R
                            • natCast_zero : NatCast.natCast 0 = 0
                            • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
                            • npow : RR
                            • npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
                            • npow_succ : ∀ (n : ) (x : R), Semiring.npow (n + 1) x = Semiring.npow n x * x
                            • mul_comm : ∀ (a b : R), a * b = b * a

                              Multiplication is commutative in a commutative multiplicative magma.

                            Instances
                              @[instance 100]
                              Equations
                              @[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
                                theorem HasDistribNeg.neg_mul {α : Type u_1} [Mul α] [self : HasDistribNeg α] (x : α) (y : α) :
                                -x * y = -(x * y)

                                Negation is left distributive over multiplication

                                theorem HasDistribNeg.mul_neg {α : Type u_1} [Mul α] [self : HasDistribNeg α] (x : α) (y : α) :
                                x * -y = -(x * y)

                                Negation is right distributive over multiplication

                                @[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
                                @[instance 100]
                                instance Ring.toNonAssocRing {α : Type u} [Ring α] :
                                Equations
                                • Ring.toNonAssocRing = let __src := inst; NonAssocRing.mk
                                @[instance 200]
                                instance instSemiring {α : Type u} [Ring α] :

                                The instance from Ring to Semiring happens often in linear algebra, for which all the basic definitions are given in terms of semirings, but many applications use rings or fields. We increase a little bit its priority above 100 to try it quickly, but remaining below the default 1000 so that more specific instances are tried first.

                                Equations
                                • instSemiring = let __src := inst; Semiring.mk Semiring.npow

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

                                Instances
                                  class NonUnitalCommRing (α : Type u) extends NonUnitalRing :

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

                                  • 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 = AddMonoid.nsmul n x + x
                                  • neg : αα
                                  • sub : ααα
                                  • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
                                  • zsmul : αα
                                  • zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
                                  • zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
                                  • zsmul_neg' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (n.succ) a
                                  • add_left_neg : ∀ (a : α), -a + a = 0
                                  • 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)
                                  • mul_comm : ∀ (a b : α), a * b = b * a

                                    Multiplication is commutative in a commutative multiplicative magma.

                                  Instances
                                    @[instance 100]
                                    Equations
                                    class CommRing (α : Type u) extends Ring :

                                    A commutative ring is a ring with commutative multiplication.

                                    Instances
                                      @[instance 100]
                                      instance CommRing.toCommSemiring {α : Type u} [s : CommRing α] :
                                      Equations
                                      @[instance 100]
                                      Equations
                                      @[instance 100]
                                      Equations
                                      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

                                          Previously an import dependency on Mathlib.Algebra.Group.Basic 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.