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
  • Multiplication is left distributive over addition

    left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
  • Multiplication is right distributive over addition

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

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

Instances
    class LeftDistribClass (R : Type u_1) [inst : Mul R] [inst : Add R] :
    • Multiplication is left distributive over addition

      left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c

    A typeclass stating that multiplication is left distributive over addition.

    Instances
      class RightDistribClass (R : Type u_1) [inst : Mul R] [inst : Add R] :
      • Multiplication is right distributive over addition

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

      A typeclass stating that multiplication is right distributive over addition.

      Instances
        instance Distrib.leftDistribClass (R : Type u_1) [inst : Distrib R] :
        Equations
        instance Distrib.rightDistribClass (R : Type u_1) [inst : Distrib R] :
        Equations
        theorem left_distrib {R : Type x} [inst : Mul R] [inst : Add R] [inst : LeftDistribClass R] (a : R) (b : R) (c : R) :
        a * (b + c) = a * b + a * c
        theorem mul_add {R : Type x} [inst : Mul R] [inst : Add R] [inst : 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} [inst : Mul R] [inst : Add R] [inst : RightDistribClass R] (a : R) (b : R) (c : R) :
        (a + b) * c = a * c + b * c
        theorem add_mul {R : Type x} [inst : Mul R] [inst : Add R] [inst : 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} [inst : Mul R] [inst : Add R] [inst : RightDistribClass R] (a : R) (b : R) (c : R) (d : R) :
        (a + b + c) * d = a * d + b * d + c * d

        Semirings #

        • Multiplication is left distributive over addition

          left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
        • Multiplication is right distributive over addition

          right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
        • Zero is a left absorbing element for multiplication

          zero_mul : ∀ (a : α), 0 * a = 0
        • Zero is a right absorbing element for multiplication

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

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

        Instances
          • Multiplication is associative

            mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

          An associative but not-necessarily unital semiring.

          Instances

            A unital but not-necessarily-associative semiring.

            Instances
              class Semiring (α : Type u) extends NonUnitalSemiring , One , NatCast :
              Instances
                theorem add_one_mul {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : RightDistribClass α] (a : α) (b : α) :
                (a + 1) * b = a * b + b
                theorem mul_add_one {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : LeftDistribClass α] (a : α) (b : α) :
                a * (b + 1) = a * b + a
                theorem one_add_mul {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : RightDistribClass α] (a : α) (b : α) :
                (1 + a) * b = b + a * b
                theorem mul_one_add {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : LeftDistribClass α] (a : α) (b : α) :
                a * (1 + b) = a + a * b
                theorem two_mul {α : Type u} [inst : NonAssocSemiring α] (n : α) :
                2 * n = n + n
                theorem bit0_eq_two_mul {α : Type u} [inst : NonAssocSemiring α] (n : α) :
                bit0 n = 2 * n
                theorem mul_two {α : Type u} [inst : NonAssocSemiring α] (n : α) :
                n * 2 = n + n
                theorem add_ite {α : Type u_1} [inst : Add α] (P : Prop) [inst : 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} [inst : Mul α] (P : Prop) [inst : 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} [inst : Add α] (P : Prop) [inst : 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} [inst : Mul α] (P : Prop) [inst : Decidable P] (a : α) (b : α) (c : α) :
                (if P then a else b) * c = if P then a * c else b * c
                theorem mul_boole {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst : Decidable P] (a : α) :
                (a * if P then 1 else 0) = if P then a else 0
                theorem boole_mul {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst : Decidable P] (a : α) :
                (if P then 1 else 0) * a = if P then a else 0
                theorem ite_mul_zero_left {α : Type u_1} [inst : MulZeroClass α] (P : Prop) [inst : Decidable P] (a : α) (b : α) :
                (if P then a * b else 0) = (if P then a else 0) * b
                theorem ite_mul_zero_right {α : Type u_1} [inst : MulZeroClass α] (P : Prop) [inst : Decidable P] (a : α) (b : α) :
                (if P then a * b else 0) = a * if P then b else 0
                theorem ite_and_mul_zero {α : Type u_1} [inst : MulZeroClass α] (P : Prop) (Q : Prop) [inst : Decidable P] [inst : Decidable Q] (a : α) (b : α) :
                (if P Q then a * b else 0) = (if P then a else 0) * if Q then b else 0
                • Multiplication is commutative in a commutative semigroup.

                  mul_comm : ∀ (a b : α), a * b = b * a

                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 :
                  • Multiplication is commutative in a commutative semigroup.

                    mul_comm : ∀ (a b : R), a * b = b * a
                  Instances
                    Equations
                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem add_mul_self_eq {α : Type u} [inst : CommSemiring α] (a : α) (b : α) :
                    (a + b) * (a + b) = a * a + 2 * a * b + b * b
                    class HasDistribNeg (α : Type u_1) [inst : Mul α] extends InvolutiveNeg :
                    Type u_1
                    • Negation is left distributive over multiplication

                      neg_mul : ∀ (x y : α), -x * y = -(x * y)
                    • Negation is right distributive over multiplication

                      mul_neg : ∀ (x y : α), x * -y = -(x * y)

                    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.

                    Instances
                      @[simp]
                      theorem neg_mul {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      -a * b = -(a * b)
                      @[simp]
                      theorem mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      a * -b = -(a * b)
                      theorem neg_mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      -a * -b = a * b
                      theorem neg_mul_eq_neg_mul {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      -(a * b) = -a * b
                      theorem neg_mul_eq_mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      -(a * b) = a * -b
                      theorem neg_mul_comm {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) :
                      -a * b = a * -b
                      theorem neg_eq_neg_one_mul {α : Type u} [inst : MulOneClass α] [inst : HasDistribNeg α] (a : α) :
                      -a = -1 * a
                      theorem mul_neg_one {α : Type u} [inst : MulOneClass α] [inst : 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} [inst : MulOneClass α] [inst : HasDistribNeg α] (a : α) :
                      -1 * a = -a

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

                      instance MulZeroClass.negZeroClass {α : Type u} [inst : MulZeroClass α] [inst : HasDistribNeg α] :
                      Equations

                      Rings #

                      class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup , Mul :
                      • Multiplication is left distributive over addition

                        left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
                      • Multiplication is right distributive over addition

                        right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
                      • Zero is a left absorbing element for multiplication

                        zero_mul : ∀ (a : α), 0 * a = 0
                      • Zero is a right absorbing element for multiplication

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

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

                      Instances
                        class NonUnitalRing (α : Type u_1) extends NonUnitalNonAssocRing :
                        Type u_1
                        • Multiplication is associative

                          mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

                        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.

                          Instances
                            class Ring (R : Type u) extends Semiring , Neg , Sub , IntCast :
                            Instances
                              Equations
                              • NonUnitalNonAssocRing.toHasDistribNeg = HasDistribNeg.mk (_ : ∀ (a b : α), -a * b = -(a * b)) (_ : ∀ (a b : α), a * -b = -(a * b))
                              theorem mul_sub_left_distrib {α : Type u} [inst : NonUnitalNonAssocRing α] (a : α) (b : α) (c : α) :
                              a * (b - c) = a * b - a * c
                              theorem mul_sub {α : Type u} [inst : NonUnitalNonAssocRing α] (a : α) (b : α) (c : α) :
                              a * (b - c) = a * b - a * c

                              Alias of mul_sub_left_distrib.

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

                              Alias of mul_sub_right_distrib.

                              theorem mul_add_eq_mul_add_iff_sub_mul_add_eq {α : Type u} [inst : NonUnitalNonAssocRing α] {a : α} {b : α} {c : α} {d : α} {e : α} :
                              a * e + c = b * e + d (a - b) * e + c = d

                              An iff statement following from right distributivity in rings and the definition of subtraction.

                              theorem sub_mul_add_eq_of_mul_add_eq_mul_add {α : Type u} [inst : NonUnitalNonAssocRing α] {a : α} {b : α} {c : α} {d : α} {e : α} (h : a * e + c = b * e + d) :
                              (a - b) * e + c = d

                              A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.

                              theorem sub_one_mul {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) :
                              (a - 1) * b = a * b - b
                              theorem mul_sub_one {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) :
                              a * (b - 1) = a * b - a
                              theorem one_sub_mul {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) :
                              (1 - a) * b = b - a * b
                              theorem mul_one_sub {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) :
                              a * (1 - b) = a - a * b
                              instance Ring.toNonUnitalRing {α : Type u} [inst : Ring α] :
                              Equations
                              instance Ring.toNonAssocRing {α : Type u} [inst : Ring α] :
                              Equations
                              • Ring.toNonAssocRing = let src := inst; NonAssocRing.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a)
                              instance instSemiring {α : Type u} [inst : Ring α] :
                              Equations
                              • instSemiring = let src := inst; Semiring.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a) Semiring.npow
                              class NonUnitalCommRing (α : Type u) extends NonUnitalRing :
                              • Multiplication is commutative in a commutative semigroup.

                                mul_comm : ∀ (a b : α), a * b = b * a

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

                              Instances
                                Equations
                                class CommRing (α : Type u) extends Ring :
                                • Multiplication is commutative in a commutative semigroup.

                                  mul_comm : ∀ (a b : α), a * b = b * a
                                Instances
                                  instance CommRing.toCommSemiring {α : Type u} [s : CommRing α] :
                                  Equations
                                  Equations
                                  Equations
                                  • CommRing.toAddCommGroupWithOne = AddCommGroupWithOne.mk
                                  class IsDomain (α : Type u) [inst : Semiring α] extends IsCancelMulZero , Nontrivial :

                                    A domain is a nontrivial semiring such 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∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c≠ 0 → a * b = a * c → b = c→ a * b = a * c → b = c→ b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c≠ 0 → a * b = c * b → a = c→ a * b = c * b → a = c→ a = c.

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

                                    Instances