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.

@[simp]

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

def AddHom.mulLeft {R : Type u_1} [Distrib R] (r : R) : AddHom 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' := (_ : ∀ (b c : R), r * (b + c) = r * b + r * c) }

@[simp]

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

def AddHom.mulRight {R : Type u_1} [Distrib R] (r : R) : AddHom 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' := (_ : ∀ (x x_1 : R), (x + x_1) * r = x * r + x_1 * r) }

@[simp, deprecated]

theorem map_bit0 {α : Type u_3} {β : Type u_2} {F : Type u_1} [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : α) : f (bit0 a) = bit0 (f a)

Additive homomorphisms preserve bit0.

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 = { toZeroHom := { toFun := fun (x : R) => r * x, map_zero' := (_ : r * 0 = 0) }, map_add' := (_ : ∀ (b c : R), r * (b + c) = r * b + r * c) }

@[simp]

theorem AddMonoidHom.coe_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : ⇑(AddMonoidHom.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 = { toZeroHom := { toFun := fun (a : R) => a * r, map_zero' := (_ : 0 * r = 0) }, map_add' := (_ : ∀ (x x_1 : R), (x + x_1) * r = x * r + x_1 * r) }

@[simp]

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

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

instance hasDistribNeg {α : Type u_1} [Mul α] [HasDistribNeg α] : HasDistribNeg αᵐᵒᵖ

Equations

• hasDistribNeg = let src := MulOpposite.involutiveNeg α; HasDistribNeg.mk (_ : ∀ (x x_1 : αᵐᵒᵖ), -x * x_1 = -(x * x_1)) (_ : ∀ (x x_1 : αᵐᵒᵖ), x * -x_1 = -(x * x_1))

@[simp]

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

theorem vieta_formula_quadratic {α : Type u_1} [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_1} [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a

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

theorem IsLeftCancelMulZero.to_noZeroDivisors (α : Type u_1) [Ring α] [IsLeftCancelMulZero α] : NoZeroDivisors α

theorem IsRightCancelMulZero.to_noZeroDivisors (α : Type u_1) [Ring α] [IsRightCancelMulZero α] : NoZeroDivisors α

instance NoZeroDivisors.to_isCancelMulZero (α : Type u_1) [Ring α] [NoZeroDivisors α] : IsCancelMulZero α

Equations

• (_ : IsCancelMulZero α) = (_ : IsCancelMulZero α)

theorem isCancelMulZero_iff_noZeroDivisors (α : Type u_1) [Ring α] : IsCancelMulZero α ↔ NoZeroDivisors α

In a ring, IsCancelMulZero and NoZeroDivisors are equivalent.

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

instance IsDomain.to_noZeroDivisors (α : Type u_1) [Ring α] [IsDomain α] : NoZeroDivisors α

Equations

• (_ : NoZeroDivisors α) = (_ : NoZeroDivisors α)

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

Equations

• (_ : IsCancelMulZero α) = (_ : IsCancelMulZero α)

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

Equations

• (_ : NoZeroDivisors α) = (_ : NoZeroDivisors α)

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

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

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

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