Mathlib.Algebra.Ring.Defs

Module docstring

{"# 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. 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 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 ","### 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 ","### Semirings ","### Rings "}

Distrib structure

(R : Type*) extends Mul R, Add R

Full source

/-- A typeclass stating that multiplication is left and right distributive
over addition. -/
class Distrib (R : Type*) extends Mul R, Add R where
  /-- Multiplication is left distributive over addition -/
  protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  /-- Multiplication is right distributive over addition -/
  protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

Distributivity of multiplication over addition

Informal description

A structure stating that for any type $ R $ equipped with multiplication and addition, the multiplication operation is both left and right distributive over addition. That is, for all $ a, b, c \in R $, the equalities $ a \cdot (b + c) = a \cdot b + a \cdot c $ (left distributivity) and $ (a + b) \cdot c = a \cdot c + b \cdot c $ (right distributivity) hold.

LeftDistribClass structure

(R : Type*) [Mul R] [Add R]

Full source

/-- A typeclass stating that multiplication is left distributive over addition. -/
class LeftDistribClass (R : Type*) [Mul R] [Add R] : Prop where
  /-- Multiplication is left distributive over addition -/
  protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c

Left distributivity of multiplication over addition

Informal description

A typeclass stating that for any type $ R $ equipped with multiplication and addition, the multiplication operation is left distributive over addition. That is, for all $ a, b, c \in R $, the equality $ a \cdot (b + c) = a \cdot b + a \cdot c $ holds.

RightDistribClass structure

(R : Type*) [Mul R] [Add R]

Full source

/-- A typeclass stating that multiplication is right distributive over addition. -/
class RightDistribClass (R : Type*) [Mul R] [Add R] : Prop where
  /-- Multiplication is right distributive over addition -/
  protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

Right distributivity of multiplication over addition

Informal description

A typeclass stating that for any type $ R $ equipped with multiplication and addition, the multiplication operation is right distributive over addition. That is, for all $ a, b, c \in R $, the equality $ (a + b) \cdot c = a \cdot c + b \cdot c $ holds.

Distrib.leftDistribClass instance

(R : Type*) [Distrib R] : LeftDistribClass R

Full source

instance (priority := 100) Distrib.leftDistribClass (R : Type*) [Distrib R] : LeftDistribClass R :=
  ⟨Distrib.left_distrib⟩

Left Distributivity in Distributive Structures

Informal description

For any type $R$ with a distributive structure (i.e., multiplication is both left and right distributive over addition), the multiplication operation is left distributive over addition. That is, for all $a, b, c \in R$, the equality $a \cdot (b + c) = a \cdot b + a \cdot c$ holds.

Distrib.rightDistribClass instance

(R : Type*) [Distrib R] : RightDistribClass R

Full source

instance (priority := 100) Distrib.rightDistribClass (R : Type*) [Distrib R] :
    RightDistribClass R :=
  ⟨Distrib.right_distrib⟩

Right Distributivity in Distributive Structures

Informal description

For any type $R$ with a distributive structure (i.e., multiplication is both left and right distributive over addition), the multiplication operation is right distributive over addition. That is, for all $a, b, c \in R$, the equality $(a + b) \cdot c = a \cdot c + b \cdot c$ holds.

left_distrib theorem

[Mul R] [Add R] [LeftDistribClass R] (a b c : R) : a * (b + c) = a * b + a * c

Full source

theorem left_distrib [Mul R] [Add R] [LeftDistribClass R] (a b c : R) :
    a * (b + c) = a * b + a * c :=
  LeftDistribClass.left_distrib a b c

Left Distributive Law: $a(b + c) = ab + ac$

Informal description

For any type $R$ equipped with multiplication and addition operations that satisfy left distributivity, and for any elements $a, b, c \in R$, the following equality holds: $$a \cdot (b + c) = a \cdot b + a \cdot c$$

right_distrib theorem

[Mul R] [Add R] [RightDistribClass R] (a b c : R) : (a + b) * c = a * c + b * c

Full source

theorem right_distrib [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
    (a + b) * c = a * c + b * c :=
  RightDistribClass.right_distrib a b c

Right Distributive Law for Multiplication over Addition

Informal description

For any type $R$ equipped with multiplication and addition operations that satisfy right distributivity, and for any elements $a, b, c \in R$, the following equality holds: $$(a + b) \cdot c = a \cdot c + b \cdot c$$

distrib_three_right theorem

[Mul R] [Add R] [RightDistribClass R] (a b c d : R) : (a + b + c) * d = a * d + b * d + c * d

Full source

theorem distrib_three_right [Mul R] [Add R] [RightDistribClass R] (a b c d : R) :
    (a + b + c) * d = a * d + b * d + c * d := by simp [right_distrib]

Right Distributive Law for Three Summands: $(a + b + c)d = ad + bd + cd$

Informal description

For any type $R$ equipped with multiplication and addition operations that satisfy right distributivity, and for any elements $a, b, c, d \in R$, the following equality holds: $$(a + b + c) \cdot d = a \cdot d + b \cdot d + c \cdot d$$

NonUnitalNonAssocSemiring structure

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

Full source

/-- 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. -/
class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α

Non-unital non-associative semiring

Informal description

A non-unital, non-associative semiring is a structure consisting of a type $\alpha$ equipped with: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ that distributes over addition (both left and right) - A zero element that is absorbing for multiplication (i.e., $0 * a = a * 0 = 0$ for all $a \in \alpha$) This structure does not require: - A multiplicative identity (unital property) - Associativity of multiplication - Commutativity of multiplication

NonUnitalSemiring structure

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

Full source

/-- An associative but not-necessarily unital semiring. -/
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α

Non-unital semiring

Informal description

A non-unital semiring is a structure consisting of a type $\alpha$ equipped with: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ that is associative and distributes over addition (both left and right) - A zero element that is absorbing for multiplication (i.e., $0 * a = a * 0 = 0$ for all $a \in \alpha$) This structure does not require: - A multiplicative identity (unital property) - Commutativity of multiplication

NonAssocSemiring structure

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

Full source

/-- A unital but not-necessarily-associative semiring. -/
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

Non-associative semiring

Informal description

A non-associative semiring is a structure consisting of a type $\alpha$ equipped with: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ that distributes over addition (both left and right) - A zero element that is absorbing for multiplication (i.e., $0 * a = a * 0 = 0$ for all $a \in \alpha$) - A multiplicative identity element (1) - A structure of an additive commutative monoid with one This structure does not require: - Associativity of multiplication - Commutativity of multiplication

NonUnitalNonAssocRing structure

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

Full source

/-- A not-necessarily-unital, not-necessarily-associative ring. -/
class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α, NonUnitalNonAssocSemiring α

Non-unital non-associative ring

Informal description

A non-unital, non-associative ring is a structure consisting of a type $\alpha$ equipped with: - An additive commutative group structure (addition and negation) - A multiplicative semigroup structure (multiplication) - Distributivity of multiplication over addition This structure does not require the existence of a multiplicative identity (unitality) nor associativity of multiplication.

NonUnitalRing structure

(α : Type*) extends NonUnitalNonAssocRing α, NonUnitalSemiring α

Full source

/-- An associative but not-necessarily unital ring. -/
class NonUnitalRing (α : Type*) extends NonUnitalNonAssocRing α, NonUnitalSemiring α

Non-unital ring

Informal description

A structure representing a non-unital ring, which is an additive commutative group equipped with a multiplication operation that is associative and distributes over addition, but does not necessarily have a multiplicative identity element.

NonAssocRing structure

(α : Type*) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
    AddCommGroupWithOne α

Full source

/-- A unital but not-necessarily-associative ring. -/
class NonAssocRing (α : Type*) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
    AddCommGroupWithOne α

Non-associative unital ring

Informal description

A structure representing a unital but not-necessarily-associative ring, which extends a non-unital non-associative ring with a multiplicative identity and an additive commutative group structure with a distinguished element 1. More precisely, a non-associative ring is a type $\alpha$ equipped with: - An additive commutative group structure (addition and negation) - A multiplicative structure with a distinguished element 1 (but not necessarily associative) - Distributivity of multiplication over addition - The property that 1 acts as a multiplicative identity

Semiring structure

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

Full source

/-- 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. -/
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

Semiring

Informal description

A semiring is a type $\alpha$ equipped with two binary operations $+$ (addition) and $*$ (multiplication), and two distinguished elements $0$ and $1$, satisfying the following properties: - Addition is commutative and associative. - Multiplication is associative and distributes over addition from both left and right. - $0$ is the additive identity and $1$ is the multiplicative identity. - Multiplication by $0$ annihilates any element. This structure extends both non-unital semirings (which lack a multiplicative identity) and non-associative semirings (which lack associativity of multiplication), while also incorporating the properties of a monoid with zero.

Ring structure

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

Full source

/-- A `Ring` is a `Semiring` with negation making it an additive group. -/
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

Ring

Informal description

A ring is a semiring equipped with an additive inverse operation, making it an additive group. It extends the structure of a semiring by adding the properties of an additive commutative group and a group with one element.

add_one_mul theorem

[RightDistribClass α] (a b : α) : (a + 1) * b = a * b + b

Full source

theorem add_one_mul [RightDistribClass α] (a b : α) : (a + 1) * b = a * b + b := by
  rw [add_mul, one_mul]

Right Distributive Property with Unit Element: $(a + 1) \cdot b = a \cdot b + b$

Informal description

For any type $\alpha$ with right-distributive multiplication over addition, and for any elements $a, b \in \alpha$, the equality $(a + 1) \cdot b = a \cdot b + b$ holds.

mul_add_one theorem

[LeftDistribClass α] (a b : α) : a * (b + 1) = a * b + a

Full source

theorem mul_add_one [LeftDistribClass α] (a b : α) : a * (b + 1) = a * b + a := by
  rw [mul_add, mul_one]

Left Distributive Property with Unit Element: $a \cdot (b + 1) = a \cdot b + a$

Informal description

For any type $\alpha$ with left-distributive multiplication over addition, and for any elements $a, b \in \alpha$, the equality $a \cdot (b + 1) = a \cdot b + a$ holds.

one_add_mul theorem

[RightDistribClass α] (a b : α) : (1 + a) * b = b + a * b

Full source

theorem one_add_mul [RightDistribClass α] (a b : α) : (1 + a) * b = b + a * b := by
  rw [add_mul, one_mul]

Right Distributive Property with Unit Element: $(1 + a) \cdot b = b + a \cdot b$

Informal description

For any type $\alpha$ with right-distributive multiplication over addition, and for any elements $a, b \in \alpha$, the equality $(1 + a) \cdot b = b + a \cdot b$ holds.

mul_one_add theorem

[LeftDistribClass α] (a b : α) : a * (1 + b) = a + a * b

Full source

theorem mul_one_add [LeftDistribClass α] (a b : α) : a * (1 + b) = a + a * b := by
  rw [mul_add, mul_one]

Left Distributive Property with Unit Element: $a \cdot (1 + b) = a + a \cdot b$

Informal description

For any type $\alpha$ with left-distributive multiplication over addition, and for any elements $a, b \in \alpha$, the equality $a \cdot (1 + b) = a + a \cdot b$ holds.

two_mul theorem

(n : α) : 2 * n = n + n

Full source

theorem two_mul (n : α) : 2 * n = n + n :=
  (congrArg₂ _ one_add_one_eq_two.symm rfl).trans <| (right_distrib 1 1 n).trans (by rw [one_mul])

Double of an element equals its sum with itself: $2n = n + n$

Informal description

For any element $n$ in a type $\alpha$ with addition and multiplication operations, the product of $2$ and $n$ equals the sum of $n$ with itself, i.e., $2 \cdot n = n + n$.

mul_two theorem

(n : α) : n * 2 = n + n

Full source

theorem mul_two (n : α) : n * 2 = n + n :=
  (congrArg₂ _ rfl one_add_one_eq_two.symm).trans <| (left_distrib n 1 1).trans (by rw [mul_one])

Multiplication by Two Equals Self-Addition: $n \cdot 2 = n + n$

Informal description

For any element $n$ in a non-associative semiring $\alpha$, the product of $n$ and $2$ equals the sum of $n$ with itself, i.e., $n \cdot 2 = n + n$.

ite_zero_mul theorem

: ite P a 0 * b = ite P (a * b) 0

Full source

lemma ite_zero_mul : ite P a 0 * b = ite P (a * b) 0 := by simp

Multiplication of Conditional Zero: $(P ? a : 0) \cdot b = P ? a \cdot b : 0$

Informal description

For any element $a$ in a type $\alpha$ with a multiplication operation and a zero element, and for any proposition $P$ and element $b \in \alpha$, the following equality holds: $$ (\text{if } P \text{ then } a \text{ else } 0) \cdot b = \text{if } P \text{ then } a \cdot b \text{ else } 0. $$

mul_ite_zero theorem

: a * ite P b 0 = ite P (a * b) 0

Full source

lemma mul_ite_zero : a * ite P b 0 = ite P (a * b) 0 := by simp

Multiplication with Conditional Zero: $a \cdot (P ? b : 0) = P ? a \cdot b : 0$

Informal description

For any element $a$ in a type $\alpha$ with a multiplication operation and a zero element, and for any proposition $P$ and element $b \in \alpha$, the following equality holds: $$ a \cdot (\text{if } P \text{ then } b \text{ else } 0) = \text{if } P \text{ then } a \cdot b \text{ else } 0. $$

ite_zero_mul_ite_zero theorem

: ite P a 0 * ite Q b 0 = ite (P ∧ Q) (a * b) 0

Full source

lemma ite_zero_mul_ite_zero : ite P a 0 * ite Q b 0 = ite (P ∧ Q) (a * b) 0 := by
  simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

Multiplication of Conditional Zeros: $(P ? a : 0) \cdot (Q ? b : 0) = (P \land Q) ? a \cdot b : 0$

Informal description

For any elements $a, b$ in a type $\alpha$ with a multiplication operation and a zero element, and for any propositions $P, Q$, the following equality holds: $$ (\text{if } P \text{ then } a \text{ else } 0) \cdot (\text{if } Q \text{ then } b \text{ else } 0) = \text{if } P \land Q \text{ then } a \cdot b \text{ else } 0. $$

mul_boole theorem

{α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) : (a * if P then 1 else 0) = if P then a else 0

Full source

theorem mul_boole {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
    (a * if P then 1 else 0) = if P then a else 0 := by simp

Multiplication by Boolean Condition: $a \cdot (P ? 1 : 0) = P ? a : 0$

Informal description

Let $\alpha$ be a type with a multiplicative identity $1$ and a zero element $0$ (i.e., a `MulZeroOneClass`), and let $P$ be a decidable proposition. For any element $a \in \alpha$, the following equality holds: $$ a \cdot (\text{if } P \text{ then } 1 \text{ else } 0) = \text{if } P \text{ then } a \text{ else } 0. $$

boole_mul theorem

{α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) : (if P then 1 else 0) * a = if P then a else 0

Full source

theorem boole_mul {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
    (if P then 1 else 0) * a = if P then a else 0 := by simp

Conditional Identity Multiplication: $(P ? 1 : 0) \cdot a = P ? a : 0$

Informal description

For any element $a$ in a type $\alpha$ with a multiplicative identity $1$ and a zero element $0$ (i.e., a `MulZeroOneClass`), and for any decidable proposition $P$, the product of the conditional expression $(if\ P\ then\ 1\ else\ 0)$ and $a$ is equal to $if\ P\ then\ a\ else\ 0$. In symbols: $$ (\text{if } P \text{ then } 1 \text{ else } 0) \cdot a = \text{if } P \text{ then } a \text{ else } 0. $$

NonUnitalNonAssocCommSemiring structure

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

Full source

/-- A not-necessarily-unital, not-necessarily-associative, but commutative semiring. -/
class NonUnitalNonAssocCommSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, CommMagma α

Non-unital non-associative commutative semiring

Informal description

A structure representing a not-necessarily-unital, not-necessarily-associative, but commutative semiring. It extends a non-unital non-associative semiring with the property that the multiplication is commutative.

NonUnitalCommSemiring structure

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

Full source

/-- 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 NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α, CommSemigroup α

Non-unital commutative semiring

Informal description

A non-unital commutative semiring is a structure consisting of a type $\alpha$ equipped with the following operations and properties: - An additive commutative monoid structure (addition is commutative and associative with a zero element) - A commutative semigroup structure (multiplication is commutative and associative) - Distributive laws (multiplication distributes over addition from both left and right) - Multiplication by zero law (multiplying any element by zero yields zero) This structure generalizes commutative semirings by not requiring a multiplicative identity element.

CommSemiring structure

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

Full source

/-- A commutative semiring is a semiring with commutative multiplication. -/
class CommSemiring (R : Type u) extends Semiring R, CommMonoid R

Commutative Semiring

Informal description

A commutative semiring is a semiring $(R, +, \cdot)$ where the multiplication operation $\cdot$ is commutative, i.e., $a \cdot b = b \cdot a$ for all $a, b \in R$. It extends the structure of a semiring by adding the commutativity condition for multiplication.

CommSemiring.toNonUnitalCommSemiring instance

[CommSemiring α] : NonUnitalCommSemiring α

Full source

instance (priority := 100) CommSemiring.toNonUnitalCommSemiring [CommSemiring α] :
    NonUnitalCommSemiring α :=
  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }

Commutative Semiring as Non-unital Commutative Semiring

Informal description

Every commutative semiring $\alpha$ is also a non-unital commutative semiring.

CommSemiring.toCommMonoidWithZero instance

[CommSemiring α] : CommMonoidWithZero α

Full source

instance (priority := 100) CommSemiring.toCommMonoidWithZero [CommSemiring α] :
    CommMonoidWithZero α :=
  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }

Commutative Semiring as Commutative Monoid with Zero

Informal description

Every commutative semiring $\alpha$ is a commutative monoid with zero.

add_mul_self_eq theorem

(a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b

Full source

theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

Expansion of $(a + b)^2$ in a commutative semiring

Informal description

For any two elements $a$ and $b$ in a commutative semiring $\alpha$, the product $(a + b) \cdot (a + b)$ expands to $a \cdot a + 2 \cdot a \cdot b + b \cdot b$.

add_sq theorem

(a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Full source

lemma add_sq (a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  simp only [sq, add_mul_self_eq]

Square of Sum Formula: $(a + b)^2 = a^2 + 2ab + b^2$

Informal description

For any two elements $a$ and $b$ in a commutative semiring $\alpha$, the square of their sum $(a + b)^2$ equals $a^2 + 2ab + b^2$.

add_sq' theorem

(a b : α) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Full source

lemma add_sq' (a b : α) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
  rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]

Square of Sum Formula (Rearranged): $(a + b)^2 = a^2 + b^2 + 2ab$

Informal description

For any two elements $a$ and $b$ in a commutative semiring $\alpha$, the square of their sum $(a + b)^2$ equals $a^2 + b^2 + 2ab$.

HasDistribNeg structure

(α : Type*) [Mul α] extends InvolutiveNeg α

Full source

/-- 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. -/
class HasDistribNeg (α : Type*) [Mul α] extends InvolutiveNeg α where
  /-- 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)

Distributive Negation

Informal description

The structure `HasDistribNeg` is a typeclass for a negation operator that distributes across multiplication. This means that for any elements $a$ and $b$ in a type $\alpha$ with multiplication, the negation satisfies $-a * b = -(a * b)$ and $a * -b = -(a * b)$. This is particularly useful for dealing with submonoids of a ring that contain $-1$ without having to duplicate lemmas.

neg_mul theorem

(a b : α) : -a * b = -(a * b)

Full source

@[simp]
theorem neg_mul (a b : α) : -a * b = -(a * b) :=
  HasDistribNeg.neg_mul _ _

Negation Distributes Over Multiplication: $-a * b = -(a * b)$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the product of $-a$ and $b$ equals the negation of the product $a * b$, i.e., $-a * b = -(a * b)$.

mul_neg theorem

(a b : α) : a * -b = -(a * b)

Full source

@[simp]
theorem mul_neg (a b : α) : a * -b = -(a * b) :=
  HasDistribNeg.mul_neg _ _

Negation Distributes Over Multiplication: $a * (-b) = -(a * b)$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the product of $a$ and $-b$ equals the negation of the product $a * b$, i.e., $a * (-b) = -(a * b)$.

neg_mul_neg theorem

(a b : α) : -a * -b = a * b

Full source

theorem neg_mul_neg (a b : α) : -a * -b = a * b := by simp

Product of Negatives: $-a \cdot -b = a \cdot b$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the product of $-a$ and $-b$ equals the product $a * b$, i.e., $-a * -b = a * b$.

neg_mul_eq_neg_mul theorem

(a b : α) : -(a * b) = -a * b

Full source

theorem neg_mul_eq_neg_mul (a b : α) : -(a * b) = -a * b :=
  (neg_mul _ _).symm

Negation of Product Equals Negated First Factor Times Second Factor: $-(a \cdot b) = (-a) \cdot b$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the negation of the product $a * b$ equals the product of the negation of $a$ and $b$, i.e., $-(a \cdot b) = (-a) \cdot b$.

neg_mul_eq_mul_neg theorem

(a b : α) : -(a * b) = a * -b

Full source

theorem neg_mul_eq_mul_neg (a b : α) : -(a * b) = a * -b :=
  (mul_neg _ _).symm

Negation of Product Equals Product with Negated Factor: $-(a * b) = a * (-b)$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the negation of the product $a * b$ equals the product of $a$ and the negation of $b$, i.e., $-(a * b) = a * (-b)$.

neg_mul_comm theorem

(a b : α) : -a * b = a * -b

Full source

theorem neg_mul_comm (a b : α) : -a * b = a * -b := by simp

Commutativity of Negation in Multiplication: $-a \cdot b = a \cdot (-b)$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with multiplication and distributive negation, the product of $-a$ and $b$ equals the product of $a$ and $-b$, i.e., $-a \cdot b = a \cdot (-b)$.

neg_eq_neg_one_mul theorem

(a : α) : -a = -1 * a

Full source

theorem neg_eq_neg_one_mul (a : α) : -a = -1 * a := by simp

Negation as Multiplication by Negative One: $-a = -1 \cdot a$

Informal description

For any element $a$ in a type $\alpha$ with multiplication and distributive negation, the negation of $a$ equals the product of $-1$ and $a$, i.e., $-a = -1 \cdot a$.

mul_neg_one theorem

(a : α) : a * -1 = -a

Full source

/-- An element of a ring multiplied by the additive inverse of one is the element's additive
  inverse. -/
theorem mul_neg_one (a : α) : a * -1 = -a := by simp

Multiplication by Negative One Yields Additive Inverse: $a \cdot (-1) = -a$

Informal description

For any element $a$ in a ring $\alpha$, the product of $a$ and $-1$ is equal to the additive inverse of $a$, i.e., $a \cdot (-1) = -a$.

neg_one_mul theorem

(a : α) : -1 * a = -a

Full source

/-- The additive inverse of one multiplied by an element of a ring is the element's additive
  inverse. -/
theorem neg_one_mul (a : α) : -1 * a = -a := by simp

Multiplication by Negative One Yields Additive Inverse: $-1 \cdot a = -a$

Informal description

For any element $a$ in a ring $\alpha$, the product of $-1$ and $a$ equals the additive inverse of $a$, i.e., $-1 \cdot a = -a$.

MulZeroClass.negZeroClass instance

: NegZeroClass α

Full source

instance (priority := 100) MulZeroClass.negZeroClass : NegZeroClass α where
  __ := inferInstanceAs (Zero α); __ := inferInstanceAs (InvolutiveNeg α)
  neg_zero := by rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]

Negation-Zero Structure from Multiplication-Zero Class

Informal description

For any type $\alpha$ equipped with a multiplication operation and a zero element (i.e., a `MulZeroClass`), there is a canonical `NegZeroClass` structure on $\alpha$ where the negation of zero is zero.

NonUnitalNonAssocRing.toHasDistribNeg instance

: HasDistribNeg α

Full source

instance (priority := 100) NonUnitalNonAssocRing.toHasDistribNeg : HasDistribNeg α where
  neg := Neg.neg
  neg_neg := neg_neg
  neg_mul a b := eq_neg_of_add_eq_zero_left <| by rw [← right_distrib, neg_add_cancel, zero_mul]
  mul_neg a b := eq_neg_of_add_eq_zero_left <| by rw [← left_distrib, neg_add_cancel, mul_zero]

Distributive Negation in Non-unital Non-associative Rings

Informal description

Every non-unital non-associative ring $\alpha$ has a distributive negation operation, meaning that for any elements $a, b \in \alpha$, we have $-a * b = -(a * b)$ and $a * -b = -(a * b)$.

mul_sub_left_distrib theorem

(a b c : α) : a * (b - c) = a * b - a * c

Full source

theorem mul_sub_left_distrib (a b c : α) : a * (b - c) = a * b - a * c := by
  simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

Left Distributive Law for Multiplication over Subtraction: $a(b - c) = ab - ac$

Informal description

For any elements $a$, $b$, and $c$ in a type $\alpha$ with multiplication and subtraction operations, the left distributive property holds: $a \cdot (b - c) = a \cdot b - a \cdot c$.

mul_sub_right_distrib theorem

(a b c : α) : (a - b) * c = a * c - b * c

Full source

theorem mul_sub_right_distrib (a b c : α) : (a - b) * c = a * c - b * c := by
  simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c

Right Distributivity of Multiplication over Subtraction: $(a - b) \cdot c = a \cdot c - b \cdot c$

Informal description

For any elements $a$, $b$, and $c$ in a type $\alpha$ with multiplication, subtraction, and distributive properties, the following equality holds: $(a - b) \cdot c = a \cdot c - b \cdot c$.

sub_one_mul theorem

(a b : α) : (a - 1) * b = a * b - b

Full source

theorem sub_one_mul (a b : α) : (a - 1) * b = a * b - b := by rw [sub_mul, one_mul]

Distributive identity: $(a - 1)b = ab - b$

Informal description

For any elements $a$ and $b$ in a non-associative unital ring $\alpha$, the following identity holds: $(a - 1) \cdot b = a \cdot b - b$.

mul_sub_one theorem

(a b : α) : a * (b - 1) = a * b - a

Full source

theorem mul_sub_one (a b : α) : a * (b - 1) = a * b - a := by rw [mul_sub, mul_one]

Right Multiplication by One Minus Identity: $a \cdot (b - 1) = a \cdot b - a$

Informal description

For any elements $a$ and $b$ in a non-associative unital ring $\alpha$, the following equality holds: $$a \cdot (b - 1) = a \cdot b - a$$

one_sub_mul theorem

(a b : α) : (1 - a) * b = b - a * b

Full source

theorem one_sub_mul (a b : α) : (1 - a) * b = b - a * b := by rw [sub_mul, one_mul]

Distributive property of $(1 - a) \cdot b$ in a non-associative ring

Informal description

For any elements $a$ and $b$ in a non-associative unital ring $\alpha$, the product of $(1 - a)$ and $b$ equals $b - a \cdot b$, i.e., $(1 - a) \cdot b = b - a \cdot b$.

mul_one_sub theorem

(a b : α) : a * (1 - b) = a - a * b

Full source

theorem mul_one_sub (a b : α) : a * (1 - b) = a - a * b := by rw [mul_sub, mul_one]

Distributive Property: $a \cdot (1 - b) = a - a \cdot b$ in a Ring

Informal description

For any elements $a$ and $b$ in a ring $\alpha$, the product of $a$ and $(1 - b)$ equals $a - a \cdot b$, i.e., $a \cdot (1 - b) = a - a \cdot b$.

Ring.toNonUnitalRing instance

: NonUnitalRing α

Full source

instance (priority := 100) Ring.toNonUnitalRing : NonUnitalRing α :=
  { ‹Ring α› with }

Rings are Non-unital Rings

Informal description

Every ring is a non-unital ring.

Ring.toNonAssocRing instance

: NonAssocRing α

Full source

instance (priority := 100) Ring.toNonAssocRing : NonAssocRing α :=
  { ‹Ring α› with }

Rings are Non-associative Unital Rings

Informal description

Every ring is a non-associative unital ring.

NonUnitalNonAssocCommRing structure

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

Full source

/-- A non-unital non-associative commutative ring is a `NonUnitalNonAssocRing` with commutative
multiplication. -/
class NonUnitalNonAssocCommRing (α : Type u)
  extends NonUnitalNonAssocRing α, NonUnitalNonAssocCommSemiring α

Non-unital non-associative commutative ring

Informal description

A non-unital non-associative commutative ring is an algebraic structure consisting of a set $\alpha$ equipped with two binary operations $+$ (addition) and $*$ (multiplication), satisfying the following properties: 1. $\alpha$ forms a non-unital non-associative ring (i.e., an additive commutative group with a multiplication that distributes over addition, but without requiring associativity of multiplication or existence of a multiplicative identity). 2. The multiplication is commutative, i.e., $a * b = b * a$ for all $a, b \in \alpha$.

NonUnitalCommRing structure

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

Full source

/-- A non-unital commutative ring is a `NonUnitalRing` with commutative multiplication. -/
class NonUnitalCommRing (α : Type u) extends NonUnitalRing α, NonUnitalNonAssocCommRing α

Non-unital commutative ring

Informal description

A non-unital commutative ring is a non-unital ring with commutative multiplication. It extends the structure of a non-unital ring by adding the property that multiplication is commutative.

NonUnitalCommRing.toNonUnitalCommSemiring instance

[s : NonUnitalCommRing α] : NonUnitalCommSemiring α

Full source

instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUnitalCommRing α] :
    NonUnitalCommSemiring α :=
  { s with }

Non-unital Commutative Rings as Non-unital Commutative Semirings

Informal description

Every non-unital commutative ring is a non-unital commutative semiring.

CommRing structure

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

Full source

/-- A commutative ring is a ring with commutative multiplication. -/
class CommRing (α : Type u) extends Ring α, CommMonoid α

Commutative Ring

Informal description

A commutative ring is a ring where the multiplication operation is commutative. It extends the structure of a ring by adding the property that for any two elements $x$ and $y$ in the ring, $x \cdot y = y \cdot x$.

CommRing.toCommSemiring instance

[s : CommRing α] : CommSemiring α

Full source

instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with }

Commutative Rings are Commutative Semirings

Informal description

Every commutative ring is a commutative semiring.

CommRing.toNonUnitalCommRing instance

[s : CommRing α] : NonUnitalCommRing α

Full source

instance (priority := 100) CommRing.toNonUnitalCommRing [s : CommRing α] : NonUnitalCommRing α :=
  { s with }

Commutative Rings as Non-Unital Commutative Rings

Informal description

Every commutative ring is a non-unital commutative ring.

CommRing.toAddCommGroupWithOne instance

[s : CommRing α] : AddCommGroupWithOne α

Full source

instance (priority := 100) CommRing.toAddCommGroupWithOne [s : CommRing α] :
    AddCommGroupWithOne α :=
  { s with }

Commutative Rings as Additive Commutative Groups with One

Informal description

Every commutative ring $\alpha$ is also an additive commutative group with one, inheriting the additive group structure along with a distinguished element $1$ and integer casting operations.

IsDomain structure

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

Full source

/-- 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 α]`. -/
@[stacks 09FE]
class IsDomain (α : Type u) [Semiring α] : Prop extends IsCancelMulZero α, Nontrivial α

Domain (cancellative semiring)

Informal description

A domain is a nontrivial semiring $\alpha$ where multiplication by any nonzero element is cancellative on both sides. That is, for all $a, b, c \in \alpha$: 1. If $a \neq 0$ and $a * b = a * c$, then $b = c$ (left cancellation). 2. If $b \neq 0$ and $a * b = c * b$, then $a = c$ (right cancellation). This is implemented as a mixin for semirings. To obtain an integral domain, one would typically combine this with a commutative ring structure (`[CommRing α] [IsDomain α]`).