Semirings and rings

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

Main definitions

• Distrib: Typeclass for distributivity of multiplication over addition.
• HasDistribNeg: Typeclass for commutativity of negation and multiplication. This is useful when dealing with multiplicative submonoids which are closed under negation without being closed under addition, for example Units.
• (NonUnital)(NonAssoc)(Semi)Ring: Typeclasses for possibly non-unital or non-associative rings and semirings. Some combinations are not defined yet because they haven't found use. For Lie Rings, there is a type synonym CommutatorRing defined in Mathlib/Algebra/Algebra/NonUnitalHom.lean turning the bracket into a multiplication so that the instance instNonUnitalNonAssocSemiringCommutatorRing can be defined.

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 : R → R → R
• add : R → R → R
• 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

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

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

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

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

@[instance 100]

instance Distrib.leftDistribClass (R : Type u_1) [Distrib R] : LeftDistribClass R

@[instance 100]

instance Distrib.rightDistribClass (R : Type u_1) [Distrib R] : RightDistribClass R

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

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α : Type u

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.

• 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

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α : Type u

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)

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α, AddCommMonoidWithOne α : Type u

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
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α, NonUnitalNonAssocSemiring α : Type u

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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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

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

An associative but not-necessarily unital 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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)

class NonAssocRing (α : Type u_1) extends NonUnitalNonAssocRing α, NonAssocSemiring α, AddCommGroupWithOne α : 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)

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

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
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x

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

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

• add : R → R → R
• 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 : ℕ → R → R
• 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 : R → R → R
• 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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)

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

@[simp]

theorem nsmul_eq_mul {α : Type u} [NonAssocSemiring α] (n : ℕ) (a : α) : n • a = ↑n * a

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

class NonUnitalNonAssocCommSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, CommMagma α : Type u

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

class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α, CommSemigroup α : Type u

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

class NonAssocCommSemiring (α : Type u) extends NonAssocSemiring α, NonUnitalNonAssocCommSemiring α : Type u

A non-associative commutative semiring is a NonAssocSemiring 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
• 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
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• mul_comm (a b : α) : a * b = b * a

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

A commutative semiring is a semiring with commutative multiplication.

• add : R → R → R
• 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 : ℕ → R → R
• 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 : R → R → R
• 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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• 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

@[implicit_reducible, instance 100]

instance NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring {α : Type u} [NonUnitalCommSemiring α] : NonUnitalNonAssocCommSemiring α

@[implicit_reducible, instance 100]

instance CommSemiring.toNonAssocCommSemiring {α : Type u} [CommSemiring α] : NonAssocCommSemiring α

@[implicit_reducible, instance 100]

instance CommSemiring.toNonUnitalCommSemiring {α : Type u} [CommSemiring α] : NonUnitalCommSemiring α

@[implicit_reducible, instance 100]

instance CommSemiring.toCommMonoidWithZero {α : Type u} [CommSemiring α] : CommMonoidWithZero α

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

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

@[implicit_reducible, instance 100]

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

Rings

@[implicit_reducible, instance 100]

instance NonUnitalNonAssocRing.toHasDistribNeg {α : Type u} [NonUnitalNonAssocRing α] : HasDistribNeg α

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

@[implicit_reducible, instance 100]

instance Ring.toNonUnitalRing {α : Type u} [Ring α] : NonUnitalRing α

@[implicit_reducible, instance 100]

instance Ring.toNonAssocRing {α : Type u} [Ring α] : NonAssocRing α

class NonUnitalNonAssocCommRing (α : Type u) extends NonUnitalNonAssocRing α, NonUnitalNonAssocCommSemiring α : Type u

A non-unital non-associative commutative ring is a NonUnitalNonAssocRing 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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_comm (a b : α) : a * b = b * a

class NonUnitalCommRing (α : Type u) extends NonUnitalRing α, NonUnitalNonAssocCommRing α : Type u

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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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

class NonAssocCommRing (α : Type u) extends NonAssocRing α, NonUnitalNonAssocCommRing α, NonAssocCommSemiring α : Type u

A non-associative commutative ring is a NonAssocRing 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : α) : a * b = b * a

@[implicit_reducible, instance 100]

instance NonUnitalCommRing.toNonUnitalCommSemiring {α : Type u} [s : NonUnitalCommRing α] : NonUnitalCommSemiring α

class CommRing (α : Type u) extends Ring α, CommMonoid α : Type u

A commutative ring is a ring 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
• 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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : α) : a * b = b * a

@[implicit_reducible, instance 100]

instance CommRing.toNonAssocCommRing {α : Type u} [CommRing α] : NonAssocCommRing α

@[implicit_reducible, instance 100]

instance CommRing.toCommSemiring {α : Type u} [s : CommRing α] : CommSemiring α

@[implicit_reducible, instance 100]

instance CommRing.toNonUnitalCommRing {α : Type u} [s : CommRing α] : NonUnitalCommRing α

@[implicit_reducible, instance 100]

instance CommRing.toAddCommGroupWithOne {α : Type u} [s : CommRing α] : AddCommGroupWithOne α

class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop

A domain is a nontrivial semiring such that multiplication by a nonzero 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 α].

• mul_left_cancel_of_ne_zero {a : α} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : α} : a ≠ 0 → IsRightRegular a
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y

@[implicit_reducible]

def IsMulCommutative.instNonUnitalNonAssocCommSemiring {R : Type v} [NonUnitalNonAssocSemiring R] [IsMulCommutative R] : NonUnitalNonAssocCommSemiring R

A NonUnitalNonAssocSemiring which IsMulCommutative is a NonUnitalNonAssocCommSemiring.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instNonUnitalCommSemiring {R : Type v} [NonUnitalSemiring R] [IsMulCommutative R] : NonUnitalCommSemiring R

A NonUnitalSemiring which IsMulCommutative is a NonUnitalCommSemiring.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instNonUnitalNonAssocCommRing {R : Type v} [NonUnitalNonAssocRing R] [IsMulCommutative R] : NonUnitalNonAssocCommRing R

A NonUnitalNonAssocRing which IsMulCommutative is a NonUnitalNonAssocCommRing.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instNonUnitalCommRing {R : Type v} [NonUnitalRing R] [IsMulCommutative R] : NonUnitalCommRing R

A NonUnitalRing which IsMulCommutative is a NonUnitalCommRing.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instNonAssocCommSemiring {R : Type v} [NonAssocSemiring R] [IsMulCommutative R] : NonAssocCommSemiring R

A NonAssocSemiring which IsMulCommutative is a NonAssocCommSemiring.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instCommSemiring {R : Type v} [Semiring R] [IsMulCommutative R] : CommSemiring R

A Semiring which IsMulCommutative is a CommSemiring.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instNonAssocCommRing {R : Type v} [NonAssocRing R] [IsMulCommutative R] : NonAssocCommRing R

A NonAssocRing which IsMulCommutative is a NonAssocCommRing.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

@[implicit_reducible]

def IsMulCommutative.instCommRing {R : Type v} [Ring R] [IsMulCommutative R] : CommRing R

A Ring which IsMulCommutative is a CommRing.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].