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.

Equations

• AddHom.mulLeft r = { toFun := fun (x : R) => r * x, map_add' := ⋯ }

@[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.

Equations

• AddHom.mulRight r = { toFun := fun (a : R) => a * r, map_add' := ⋯ }

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

Equations

• AddMonoidHom.mulLeft r = { toFun := fun (x : R) => r * x, map_zero' := ⋯, map_add' := ⋯ }

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

Equations

• AddMonoidHom.mulRight r = { toFun := fun (a : R) => a * r, map_zero' := ⋯, map_add' := ⋯ }

@[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.

Equations

• AddMonoidHom.mul = { toFun := AddMonoidHom.mulLeft, map_zero' := ⋯, map_add' := ⋯ }

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.

Equations

• AddMonoid.End.mulLeft = AddMonoidHom.mul

@[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.

Equations

• AddMonoid.End.mulRight = AddMonoidHom.mul.flip

@[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 αᵐᵒᵖ

Equations

• MulOpposite.instHasDistribNeg = { toInvolutiveNeg := MulOpposite.instInvolutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

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 α

theorem isLeftRegular_iff_right_eq_zero_of_mul {R : Type u_3} [NonUnitalNonAssocRing R] {r : R} : IsLeftRegular r ↔ ∀ (x : R), r * x = 0 → x = 0

theorem isRightRegular_iff_left_eq_zero_of_mul {R : Type u_3} [NonUnitalNonAssocRing R] {r : R} : IsRightRegular r ↔ ∀ (x : R), x * r = 0 → x = 0

theorem isRegular_iff_eq_zero_of_mul {R : Type u_3} [NonUnitalNonAssocRing R] {r : R} : IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

theorem noZeroDivisors_tfae {R : Type u_3} [NonUnitalNonAssocRing R] : [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

A (not necessarily unital or associative) ring with no zero divisors has cancellative multiplication on both sides. Since either left or right cancellative multiplication implies the absence of zero divisors, the four conditions are equivalent to each other.

theorem isCancelMulZero_iff_noZeroDivisors {R : Type u_3} [NonUnitalNonAssocRing R] : IsCancelMulZero R ↔ NoZeroDivisors R

In a ring, IsCancelMulZero and NoZeroDivisors are equivalent.

@[instance 100]

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

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 α

theorem 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