Semirings and rings

This file gives lemmas about semirings, rings and domains. This is analogous to Algebra.Group.Basic, the difference being that the former is about + and * separately, while the present file is about their interaction.

For the definitions of semirings and rings see Algebra.Ring.Defs.

def AddHom.mulLeft {R : Type u_1} [Distrib R] (r : R) : R →ₙ+ R

Left multiplication by an element of a type with distributive multiplication is an AddHom.

@[simp]

theorem AddHom.mulLeft_apply {R : Type u_1} [Distrib R] (r : R) : ⇑(mulLeft r) = fun (x : R) => r * x

def AddHom.mulRight {R : Type u_1} [Distrib R] (r : R) : R →ₙ+ R

Left multiplication by an element of a type with distributive multiplication is an AddHom.

@[simp]

theorem AddHom.mulRight_apply {R : Type u_1} [Distrib R] (r : R) : ⇑(mulRight r) = fun (a : R) => a * r

def AddMonoidHom.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : R →+ R

Left multiplication by an element of a (semi)ring is an AddMonoidHom

@[simp]

theorem AddMonoidHom.coe_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : ⇑(mulLeft r) = HMul.hMul r

def AddMonoidHom.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : R →+ R

Right multiplication by an element of a (semi)ring is an AddMonoidHom

@[simp]

theorem AddMonoidHom.coe_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : ⇑(mulRight r) = fun (x : R) => x * r

theorem AddMonoidHom.mulRight_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (a r : R) : (mulRight r) a = a * r

def AddMonoidHom.mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R

Multiplication of an element of a (semi)ring is an AddMonoidHom in both arguments.

This is a more-strongly bundled version of AddMonoidHom.mulLeft and AddMonoidHom.mulRight.

Stronger versions of this exists for algebras as LinearMap.mul, NonUnitalAlgHom.mul and Algebra.lmul.

theorem AddMonoidHom.mul_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x y : R) : (mul x) y = x * y

@[simp]

theorem AddMonoidHom.coe_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑mul = mulLeft

@[simp]

theorem AddMonoidHom.coe_flip_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑mul.flip = mulRight

theorem AddMonoidHom.map_mul_iff {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →+ S) : (∀ (x y : R), f (x * y) = f x * f y) ↔ mul.compr₂ f = (mul.comp f).compl₂ f

An AddMonoidHom preserves multiplication if pre- and post- composition with mul are equivalent. By converting the statement into an equality of AddMonoidHoms, this lemma allows various specialized ext lemmas about →+ to then be applied.

theorem AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {a : R} : mulLeft a = mulRight a ↔ ∀ (b : R), Commute a b

theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {b : R} : mulRight b = mulLeft b ↔ ∀ (a : R), Commute a b

def AddMonoid.End.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The left multiplication map: (a, b) ↦ a * b. See also AddMonoidHom.mulLeft.

@[simp]

theorem AddMonoid.End.mulLeft_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (r x✝ : R) : (mulLeft r) x✝ = r * x✝

def AddMonoid.End.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The right multiplication map: (a, b) ↦ b * a. See also AddMonoidHom.mulRight.

@[simp]

theorem AddMonoid.End.mulRight_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (y x : R) : (mulRight y) x = x * y

theorem AddMonoid.End.mulRight_eq_mulLeft {R : Type u_1} [NonUnitalNonAssocCommSemiring R] : mulRight = mulLeft

instance MulOpposite.instHasDistribNeg {α : Type u_3} [Mul α] [HasDistribNeg α] : HasDistribNeg αᵐᵒᵖ

theorem vieta_formula_quadratic {α : Type u_3} [NonUnitalCommRing α] {b c x : α} (h : x * x - b * x + c = 0) : ∃ (y : α), y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with its roots. This particular version states that if we have a root x of a monic quadratic polynomial, then there is another root y such that x + y is negative the a_1 coefficient and x * y is the a_0 coefficient.

theorem succ_ne_self {α : Type u_3} [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a

theorem pred_ne_self {α : Type u_3} [NonAssocRing α] [Nontrivial α] (a : α) : a - 1 ≠ a

theorem IsLeftCancelMulZero.to_noZeroDivisors (α : Type u_3) [MulZeroClass α] [IsLeftCancelMulZero α] : NoZeroDivisors α

theorem IsRightCancelMulZero.to_noZeroDivisors (α : Type u_3) [MulZeroClass α] [IsRightCancelMulZero α] : NoZeroDivisors α

@[instance 100]

instance NoZeroDivisors.to_isCancelMulZero (α : Type u_3) [NonUnitalNonAssocRing α] [NoZeroDivisors α] : IsCancelMulZero α

theorem isCancelMulZero_iff_noZeroDivisors (α : Type u_3) [NonUnitalNonAssocRing α] : IsCancelMulZero α ↔ NoZeroDivisors α

In a ring, IsCancelMulZero and NoZeroDivisors are equivalent.

theorem NoZeroDivisors.to_isDomain (α : Type u_3) [Ring α] [h : Nontrivial α] [NoZeroDivisors α] : IsDomain α

@[instance 100]

instance IsDomain.to_noZeroDivisors (α : Type u_3) [Semiring α] [IsDomain α] : NoZeroDivisors α

instance Subsingleton.to_isCancelMulZero (α : Type u_3) [Mul α] [Zero α] [Subsingleton α] : IsCancelMulZero α

instance Subsingleton.to_noZeroDivisors (α : Type u_3) [Mul α] [Zero α] [Subsingleton α] : NoZeroDivisors α

theorem isDomain_iff_cancelMulZero_and_nontrivial (α : Type u_3) [Semiring α] : IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α

theorem isCancelMulZero_iff_isDomain_or_subsingleton (α : Type u_3) [Semiring α] : IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

theorem isDomain_iff_noZeroDivisors_and_nontrivial (α : Type u_3) [Ring α] : IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

theorem noZeroDivisors_iff_isDomain_or_subsingleton (α : Type u_3) [Ring α] : NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

theorem one_div_neg_one_eq_neg_one {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] : 1 / -1 = -1

theorem one_div_neg_eq_neg_one_div {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a : R) : 1 / -a = -(1 / a)

theorem div_neg_eq_neg_div {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a b : R) : b / -a = -(b / a)

theorem neg_div {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a b : R) : -b / a = -(b / a)

theorem neg_div' {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a b : R) : -(b / a) = -b / a

@[simp]

theorem neg_div_neg_eq {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a b : R) : -a / -b = a / b

theorem neg_inv {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] {a : R} : -a⁻¹ = (-a)⁻¹

theorem div_neg {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] {b : R} (a : R) : a / -b = -(a / b)

@[simp]

theorem inv_neg {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] {a : R} : (-a)⁻¹ = -a⁻¹

@[deprecated inv_neg (since := "2025-04-24")]

theorem inv_neg' {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] {a : R} : (-a)⁻¹ = -a⁻¹

Alias of inv_neg.

theorem inv_neg_one {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] : (-1)⁻¹ = -1