# 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} [] (r : R) :
= fun (x : R) => r * x
def AddHom.mulLeft {R : Type u_1} [] (r : R) :

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

Equations
• = { toFun := fun (x : R) => r * x, map_add' := }
Instances For
@[simp]
theorem AddHom.mulRight_apply {R : Type u_1} [] (r : R) :
= fun (a : R) => a * r
def AddHom.mulRight {R : Type u_1} [] (r : R) :

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

Equations
• = { toFun := fun (a : R) => a * r, map_add' := }
Instances For
def AddMonoidHom.mulLeft {R : Type u_1} (r : R) :
R →+ R

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

Equations
• = { toFun := fun (x : R) => r * x, map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddMonoidHom.coe_mulLeft {R : Type u_1} (r : R) :
def AddMonoidHom.mulRight {R : Type u_1} (r : R) :
R →+ R

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

Equations
• = { toFun := fun (a : R) => a * r, map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddMonoidHom.coe_mulRight {R : Type u_1} (r : R) :
= fun (x : R) => x * r
theorem AddMonoidHom.mulRight_apply {R : Type u_1} (a : R) (r : R) :
= a * r
instance instHasDistribNeg {α : Type u_2} [Mul α] [] :
Equations
• instHasDistribNeg =
@[simp]
theorem inv_neg' {α : Type u_2} [] [] (a : α) :
theorem vieta_formula_quadratic {α : Type u_2} {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_2} [] [] (a : α) :
a + 1 a
theorem pred_ne_self {α : Type u_2} [] [] (a : α) :
a - 1 a
@[instance 100]
instance NoZeroDivisors.to_isCancelMulZero (α : Type u_2) [] :
Equations
• =

In a ring, IsCancelMulZero and NoZeroDivisors are equivalent.

theorem NoZeroDivisors.to_isDomain (α : Type u_2) [Ring α] [h : ] [] :
@[instance 100]
instance IsDomain.to_noZeroDivisors (α : Type u_2) [Ring α] [] :
Equations
• =
instance Subsingleton.to_isCancelMulZero (α : Type u_2) [Mul α] [Zero α] [] :
Equations
• =
instance Subsingleton.to_noZeroDivisors (α : Type u_2) [Mul α] [Zero α] [] :
Equations
• =