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

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

Tags

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

Distrib class

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

• 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

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

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

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

  Multiplication is left distributive over addition

A typeclass stating that multiplication is left distributive over addition.

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

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

  Multiplication is right distributive over addition

A typeclass stating that multiplication is right distributive over addition.

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

Equations

• Distrib.leftDistribClass = Distrib.leftDistribClass.proof_1

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

Equations

• Distrib.rightDistribClass = Distrib.rightDistribClass.proof_1

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

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid , Mul : Type u

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

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

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

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

An associative but not-necessarily unital semiring.

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring , One , NatCast : Type u

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

A unital but not-necessarily-associative semiring.

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

• 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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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

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

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

• 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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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)

  Multiplication is associative

An associative but not-necessarily unital ring.

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

• 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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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 homorphism ℤ → R agrees with the one from ℕ → R on ℕ.

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

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

A unital but not-necessarily-associative ring.

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

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

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

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → R → R
• npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (a : R), -a + a = 0
• intCast : ℤ → R
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n

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

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

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

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

theorem ite_mul_zero_left {α : Type u_1} [MulZeroClass α] (P : Prop) [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} [MulZeroClass α] (P : Prop) [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} [MulZeroClass α] (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) : (if P ∧ Q then a * b else 0) = (if P then a else 0) * if Q then b else 0

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

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

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

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → R → R
• npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = x * Semiring.npow n x
• mul_comm : ∀ (a b : R), a * b = b * a

  Multiplication is commutative in a commutative semigroup.

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

Equations

• CommSemiring.toNonUnitalCommSemiring = let src := inferInstanceAs (CommMonoid α); let src_1 := inferInstanceAs (CommSemiring α); NonUnitalCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• One or more equations did not get rendered due to their size.

theorem add_mul_self_eq {α : Type u} [CommSemiring α] (a : α) (b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b

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

• 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

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.

@[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 MulZeroClass.negZeroClass {α : Type u} [MulZeroClass α] [HasDistribNeg α] : NegZeroClass α

Equations

• MulZeroClass.negZeroClass = let src := inferInstanceAs (Zero α); let src_1 := inferInstanceAs (InvolutiveNeg α); NegZeroClass.mk (_ : -0 = 0)

Rings

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

Equations

• NonUnitalNonAssocRing.toHasDistribNeg = HasDistribNeg.mk (_ : ∀ (a b : α), -a * b = -(a * b)) (_ : ∀ (a b : α), a * -b = -(a * b))

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 Ring.toNonUnitalRing {α : Type u} [Ring α] : NonUnitalRing α

Equations

• Ring.toNonUnitalRing = let src := inst; NonUnitalRing.mk (_ : ∀ (a b c : α), a * b * c = a * (b * c))

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

Equations

• Ring.toNonAssocRing = let src := inst; NonAssocRing.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a)

instance instSemiring {α : Type u} [Ring α] : Semiring α

Equations

• instSemiring = let src := inst; Semiring.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a) Semiring.npow

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

• 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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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 semigroup.

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

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

Equations

• NonUnitalCommRing.toNonUnitalCommSemiring = NonUnitalCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  Multiplication is commutative in a commutative semigroup.

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

Equations

• CommRing.toCommSemiring = CommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• CommRing.toNonUnitalCommRing = NonUnitalCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• CommRing.toAddCommGroupWithOne = AddCommGroupWithOne.mk

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

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 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 α].

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.