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

ink

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

• Multiplication is left distributive over addition

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

• Multiplication is right distributive over addition

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

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

ink

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

• Multiplication is left distributive over addition

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

A typeclass stating that multiplication is left distributive over addition.

ink

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

• Multiplication is right distributive over addition

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

A typeclass stating that multiplication is right distributive over addition.

ink

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

Equations

• Distrib.leftDistribClass R = { left_distrib := (_ : ∀ (a b c : R), a * (b + c) = a * b + a * c) }

ink

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

Equations

• Distrib.rightDistribClass R = { right_distrib := (_ : ∀ (a b c : R), (a + b) * c = a * c + b * c) }

ink

theorem left_distrib {R : Type x} [inst : Mul R] [inst : Add R] [inst : LeftDistribClass R] (a : R) (b : R) (c : R) : a * (b + c) = a * b + a * c

ink

theorem mul_add {R : Type x} [inst : Mul R] [inst : Add R] [inst : LeftDistribClass R] (a : R) (b : R) (c : R) : a * (b + c) = a * b + a * c

Alias of left_distrib.

ink

theorem right_distrib {R : Type x} [inst : Mul R] [inst : Add R] [inst : RightDistribClass R] (a : R) (b : R) (c : R) : (a + b) * c = a * c + b * c

ink

theorem add_mul {R : Type x} [inst : Mul R] [inst : Add R] [inst : RightDistribClass R] (a : R) (b : R) (c : R) : (a + b) * c = a * c + b * c

Alias of right_distrib.

ink

theorem distrib_three_right {R : Type x} [inst : Mul R] [inst : Add R] [inst : RightDistribClass R] (a : R) (b : R) (c : R) (d : R) : (a + b + c) * d = a * d + b * d + c * d

Semirings

ink

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

• Multiplication is left distributive over addition

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

• Multiplication is right distributive over addition

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

• Zero is a left absorbing element for multiplication

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

• Zero is a right absorbing element for multiplication

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

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

ink

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

• Multiplication is associative

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

An associative but not-necessarily unital semiring.

ink

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

• One is a right neutral element for multiplication

  mul_one : ∀ (a : α), a * 1 = a
• toNatCast : NatCast α

• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

  natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝

• The canonical map ℕ → R→ R is a homomorphism.

  natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝

A unital but not-necessarily-associative semiring.

ink

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

• One is a right neutral element for multiplication

  mul_one : ∀ (a : α), a * 1 = a
• toNatCast : NatCast α

• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

  natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝

• The canonical map ℕ → R→ R is a homomorphism.

  natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝

• Raising to the power of a natural number.

  npow : ℕ → α → α

• Raising to the power (0 : ℕ) gives 1.

  npow_zero : autoParam (∀ (x : α), npow 0 x = 1) _auto✝

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

  npow_succ : autoParam (∀ (n : ℕ) (x : α), npow (n + 1) x = x * npow n x) _auto✝

ink

theorem add_one_mul {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : RightDistribClass α] (a : α) (b : α) : (a + 1) * b = a * b + b

ink

theorem mul_add_one {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : LeftDistribClass α] (a : α) (b : α) : a * (b + 1) = a * b + a

ink

theorem one_add_mul {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : RightDistribClass α] (a : α) (b : α) : (1 + a) * b = b + a * b

ink

theorem mul_one_add {α : Type u} [inst : Add α] [inst : MulOneClass α] [inst : LeftDistribClass α] (a : α) (b : α) : a * (1 + b) = a + a * b

ink

theorem two_mul {α : Type u} [inst : NonAssocSemiring α] (n : α) : 2 * n = n + n

ink

theorem bit0_eq_two_mul {α : Type u} [inst : NonAssocSemiring α] (n : α) : bit0 n = 2 * n

ink

theorem mul_two {α : Type u} [inst : NonAssocSemiring α] (n : α) : n * 2 = n + n

ink

theorem add_ite {α : Type u_1} [inst : Add α] (P : Prop) [inst : Decidable P] (a : α) (b : α) (c : α) : (a + if P then b else c) = if P then a + b else a + c

ink

@[simp]

theorem mul_ite {α : Type u_1} [inst : Mul α] (P : Prop) [inst : Decidable P] (a : α) (b : α) (c : α) : (a * if P then b else c) = if P then a * b else a * c

ink

theorem ite_add {α : Type u_1} [inst : Add α] (P : Prop) [inst : Decidable P] (a : α) (b : α) (c : α) : (if P then a else b) + c = if P then a + c else b + c

ink

@[simp]

theorem ite_mul {α : Type u_1} [inst : Mul α] (P : Prop) [inst : Decidable P] (a : α) (b : α) (c : α) : (if P then a else b) * c = if P then a * c else b * c

ink

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

ink

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

ink

theorem ite_mul_zero_left {α : Type u_1} [inst : MulZeroClass α] (P : Prop) [inst : Decidable P] (a : α) (b : α) : (if P then a * b else 0) = (if P then a else 0) * b

ink

theorem ite_mul_zero_right {α : Type u_1} [inst : MulZeroClass α] (P : Prop) [inst : Decidable P] (a : α) (b : α) : (if P then a * b else 0) = a * if P then b else 0

ink

theorem ite_and_mul_zero {α : Type u_1} [inst : MulZeroClass α] (P : Prop) (Q : Prop) [inst : Decidable P] [inst : Decidable Q] (a : α) (b : α) : (if P ∧ Q then a * b else 0) = (if P then a else 0) * if Q then b else 0

ink

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

• Multiplication is commutative in a commutative semigroup.

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

A non-unital commutative semiring is a NonUnitalSemiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (AddCommMonoid), commutative semigroup (CommSemigroup), distributive laws (Distrib), and multiplication by zero law (MulZeroClass).

ink

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

• Multiplication is commutative in a commutative semigroup.

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

ink

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

• Negation is left distributive over multiplication

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

• Negation is right distributive over multiplication

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

Typeclass for a negation operator that distributes across multiplication.

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

ink

@[simp]

theorem neg_mul {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : -a * b = -(a * b)

ink

@[simp]

theorem mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : a * -b = -(a * b)

ink

theorem neg_mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : -a * -b = a * b

ink

theorem neg_mul_eq_neg_mul {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : -(a * b) = -a * b

ink

theorem neg_mul_eq_mul_neg {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : -(a * b) = a * -b

ink

theorem neg_mul_comm {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] (a : α) (b : α) : -a * b = a * -b

ink

theorem neg_eq_neg_one_mul {α : Type u} [inst : MulOneClass α] [inst : HasDistribNeg α] (a : α) : -a = -1 * a

ink

theorem mul_neg_one {α : Type u} [inst : MulOneClass α] [inst : HasDistribNeg α] (a : α) : a * -1 = -a

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

ink

theorem neg_one_mul {α : Type u} [inst : MulOneClass α] [inst : HasDistribNeg α] (a : α) : -1 * a = -a

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

ink

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

Equations

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

Rings

ink

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

• Multiplication is left distributive over addition

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

• Multiplication is right distributive over addition

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

• Zero is a left absorbing element for multiplication

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

• Zero is a right absorbing element for multiplication

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

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

ink

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

• Multiplication is associative

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

An associative but not-necessarily unital ring.

ink

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

• toNatCast : NatCast α

• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

  natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝

• The canonical map ℕ → R→ R is a homomorphism.

  natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝
• toIntCast : IntCast α

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

  intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝

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

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

A unital but not-necessarily-associative ring.

ink

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

• zsmul : ℤ → R → R
• zsmul_zero' : autoParam (∀ (a : R), zsmul 0 a = 0) _auto✝
• zsmul_succ' : autoParam (∀ (n : ℕ) (a : R), zsmul (Int.ofNat (Nat.succ n)) a = a + zsmul (Int.ofNat n) a) _auto✝
• zsmul_neg' : autoParam (∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑(Nat.succ n)) a) _auto✝
• add_left_neg : ∀ (a : R), -a + a = 0
• toIntCast : IntCast R

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

  intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝

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

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

ink

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

Equations

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

ink

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

ink

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

Alias of mul_sub_left_distrib.

ink

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

ink

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

Alias of mul_sub_right_distrib.

ink

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

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

ink

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

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

ink

theorem sub_one_mul {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) : (a - 1) * b = a * b - b

ink

theorem mul_sub_one {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) : a * (b - 1) = a * b - a

ink

theorem one_sub_mul {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) : (1 - a) * b = b - a * b

ink

theorem mul_one_sub {α : Type u} [inst : NonAssocRing α] (a : α) (b : α) : a * (1 - b) = a - a * b

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

• Multiplication is commutative in a commutative semigroup.

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

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

ink

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

Equations

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

ink

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

• Multiplication is commutative in a commutative semigroup.

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• CommRing.toAddCommGroupWithOne = AddCommGroupWithOne.mk

ink

class IsDomain (α : Type u) [inst : 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∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c≠ 0 → a * b = a * c → b = c→ a * b = a * c → b = c→ b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c≠ 0 → a * b = c * b → a = c→ a * b = c * b → a = c→ a = c.

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