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

source
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

Instances

source
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

Instances

source
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

Instances

source
@[instance 100]
instance Distrib.leftDistribClass (R : Type u_1) [Distrib R] :
LeftDistribClass R
source
@[instance 100]
instance Distrib.rightDistribClass (R : Type u_1) [Distrib R] :
RightDistribClass R
source
theorem left_distrib {R : Type v} [Mul R] [Add R] [LeftDistribClass R] (a b c : R) :
a * (b + c) = a * b + a * c
source
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`.

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

source
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

source
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

Instances

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

Instances

source
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

Instances

source
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

Instances

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

Instances

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

Instances

source
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

Instances

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

Instances

### Semirings #

source
theorem add_one_mul {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
(a + 1) * b = a * b + b
source
theorem mul_add_one {α : Type u} [Add α] [MulOneClass α] [LeftDistribClass α] (a b : α) :
a * (b + 1) = a * b + a
source
theorem one_add_mul {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
(1 + a) * b = b + a * b
source
theorem mul_one_add {α : Type u} [Add α] [MulOneClass α] [LeftDistribClass α] (a b : α) :
a * (1 + b) = a + a * b
source
theorem two_mul {α : Type u} [NonAssocSemiring α] (n : α) :
2 * n = n + n
source
theorem mul_two {α : Type u} [NonAssocSemiring α] (n : α) :
n * 2 = n + n
source
@[simp]
theorem nsmul_eq_mul {α : Type u} [NonAssocSemiring α] (n : ℕ) (a : α) :
n • a = ↑n * a
source
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
source
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
source
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
source
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
source
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
source
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

Instances

source
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

Instances

source
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

Instances

source
@[instance 100]
instance CommSemiring.toNonUnitalCommSemiring {α : Type u} [CommSemiring α] :
NonUnitalCommSemiring α
Equations

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

source
@[instance 100]
instance CommSemiring.toCommMonoidWithZero {α : Type u} [CommSemiring α] :
CommMonoidWithZero α
Equations

- CommSemiring.toCommMonoidWithZero = { toCommMonoid := inferInstanceAs (CommMonoid α), toZero := (inferInstanceAs (CommSemiring α)).toZero, zero_mul := ⋯, mul_zero := ⋯ }

source
theorem add_mul_self_eq {α : Type u} [CommSemiring α] (a b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
source
theorem add_sq {α : Type u} [CommSemiring α] (a b : α) :
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
source
theorem add_sq' {α : Type u} [CommSemiring α] (a b : α) :
(a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
source
theorem add_pow_two {α : Type u} [CommSemiring α] (a b : α) :
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Alias of `add_sq`.

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

Typeclass for a negation operator that distributes across multiplication.

This is useful for dealing with submonoids of a ring that contain `-1` without having to duplicate lemmas.

- neg : α → α
- neg_neg (x : α) : - -x = x
- neg_mul (x y : α) : -x * y = -(x * y)

  Negation is left distributive over multiplication

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

  Negation is right distributive over multiplication

Instances

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

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

source
@[instance 100]
instance MulZeroClass.negZeroClass {α : Type u} [MulZeroClass α] [HasDistribNeg α] :
NegZeroClass α
Equations

- MulZeroClass.negZeroClass = { toZero := inferInstanceAs (Zero α), toNeg := (inferInstanceAs (InvolutiveNeg α)).toNeg, neg_zero := ⋯ }

### Rings #

source
@[instance 100]
instance NonUnitalNonAssocRing.toHasDistribNeg {α : Type u} [NonUnitalNonAssocRing α] :
HasDistribNeg α
Equations

- NonUnitalNonAssocRing.toHasDistribNeg = { toNeg := inst✝.toNeg, neg_neg := ⋯, neg_mul := ⋯, mul_neg := ⋯ }

source
theorem mul_sub_left_distrib {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
a * (b - c) = a * b - a * c
source
theorem mul_sub {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) :
a * (b - c) = a * b - a * c

Alias of `mul_sub_left_distrib`.

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

Alias of `mul_sub_right_distrib`.

source
theorem sub_one_mul {α : Type u} [NonAssocRing α] (a b : α) :
(a - 1) * b = a * b - b
source
theorem mul_sub_one {α : Type u} [NonAssocRing α] (a b : α) :
a * (b - 1) = a * b - a
source
theorem one_sub_mul {α : Type u} [NonAssocRing α] (a b : α) :
(1 - a) * b = b - a * b
source
theorem mul_one_sub {α : Type u} [NonAssocRing α] (a b : α) :
a * (1 - b) = a - a * b
source
@[instance 100]
instance Ring.toNonUnitalRing {α : Type u} [Ring α] :
NonUnitalRing α
Equations

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

source
@[instance 100]
instance Ring.toNonAssocRing {α : Type u} [Ring α] :
NonAssocRing α
Equations

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

source
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

Instances

source
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

Instances

source
@[instance 100]
instance NonUnitalCommRing.toNonUnitalCommSemiring {α : Type u} [s : NonUnitalCommRing α] :
NonUnitalCommSemiring α
Equations

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

source
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

Instances

source
@[instance 100]
instance CommRing.toCommSemiring {α : Type u} [s : CommRing α] :
CommSemiring α
Equations

- CommRing.toCommSemiring = { toSemiring := s.toSemiring, mul_comm := ⋯ }

source
@[instance 100]
instance CommRing.toNonUnitalCommRing {α : Type u} [s : CommRing α] :
NonUnitalCommRing α
Equations

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

source
@[instance 100]
instance CommRing.toAddCommGroupWithOne {α : Type u} [s : CommRing α] :
AddCommGroupWithOne α
Equations

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

source
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

Instances