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.

source

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' := ⋯ }

Instances For

source

@[simp]

theorem AddHom.mulLeft_apply {R : Type u_1} [Distrib R] (r : R) :

⇑(AddHom.mulLeft r) = fun (x : R) => r * x

source

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' := ⋯ }

Instances For

source

@[simp]

theorem AddHom.mulRight_apply {R : Type u_1} [Distrib R] (r : R) :

⇑(AddHom.mulRight r) = fun (a : R) => a * r

source

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' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.coe_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) :

⇑(AddMonoidHom.mulLeft r) = HMul.hMul r

source

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' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.coe_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) :

⇑(AddMonoidHom.mulRight r) = fun (x : R) => x * r

source

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

(AddMonoidHom.mulRight r) a = a * r

source

instance instHasDistribNeg {α : Type u_2} [Mul α] [HasDistribNeg α] :

HasDistribNeg αᵐᵒᵖ

Equations

instHasDistribNeg = HasDistribNeg.mk ⋯ ⋯

source

@[simp]

theorem inv_neg' {α : Type u_2} [Group α] [HasDistribNeg α] (a : α) :

(-a)⁻¹ = -a⁻¹

source

theorem vieta_formula_quadratic {α : Type u_2} [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.

source