Documentation

Mathlib.Algebra.Ring.Basic

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
ink
@[simp]
theorem AddHom.mulLeft_apply {R : Type u_1} [inst : Distrib R] (r : R) :
↑(AddHom.mulLeft r) = (fun x x_1 => x * x_1) r
source
ink
def AddHom.mulLeft {R : Type u_1} [inst : 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 x_1 => x * x_1) r, map_add' := (_ : ∀ (b c : R), r * (b + c) = r * b + r * c) }
source
ink
@[simp]
theorem AddHom.mulRight_apply {R : Type u_1} [inst : Distrib R] (r : R) :
↑(AddHom.mulRight r) = fun a => a * r
source
ink
def AddHom.mulRight {R : Type u_1} [inst : 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 => a * r, map_add' := (_ : ∀ (x x_1 : R), (x + x_1) * r = x * r + x_1 * r) }
source
ink
@[simp]
theorem map_bit0 {α : Type u_2} {β : Type u_1} {F : Type u_3} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] [inst : AddHomClass F α β] (f : F) (a : α) :
↑f (bit0 a) = bit0 (↑f a)

Additive homomorphisms preserve bit0.

source
ink
def AddMonoidHom.mulLeft {R : Type u_1} [inst : 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 x_1 => x * x_1) r, map_zero' := (_ : r * 0 = 0) }, map_add' := (_ : ∀ (b c : R), r * (b + c) = r * b + r * c) }
source
ink
@[simp]
theorem AddMonoidHom.coe_mul_left {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (r : R) :
↑(AddMonoidHom.mulLeft r) = HMul.hMul r
source
ink
def AddMonoidHom.mulRight {R : Type u_1} [inst : 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 => a * r, map_zero' := (_ : 0 * r = 0) }, map_add' := (_ : ∀ (x x_1 : R), (x + x_1) * r = x * r + x_1 * r) }
source
ink
@[simp]
theorem AddMonoidHom.coe_mul_right {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (r : R) :
↑(AddMonoidHom.mulRight r) = fun x => x * r
source
ink
theorem AddMonoidHom.mul_right_apply {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (a : R) (r : R) :
↑(AddMonoidHom.mulRight r) a = a * r
source
ink
instance hasDistribNeg {α : Type u_1} [inst : Mul α] [inst : HasDistribNeg α] :
HasDistribNeg αᵐᵒᵖ
Equations
source
ink
@[simp]
theorem inv_neg' {α : Type u_1} [inst : Group α] [inst : HasDistribNeg α] (a : α) :
(-a)⁻¹ = -a⁻¹
source
ink
theorem vieta_formula_quadratic {α : Type u_1} [inst : 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
ink
theorem succ_ne_self {α : Type u_1} [inst : NonAssocRing α] [inst : Nontrivial α] (a : α) :
a + 1 ≠ a
source
ink
theorem pred_ne_self {α : Type u_1} [inst : NonAssocRing α] [inst : Nontrivial α] (a : α) :
a - 1 ≠ a
source
ink
theorem IsLeftCancelMulZero.to_noZeroDivisors (α : Type u_1) [inst : Ring α] [inst : IsLeftCancelMulZero α] :
NoZeroDivisors α
source
ink
theorem IsRightCancelMulZero.to_noZeroDivisors (α : Type u_1) [inst : Ring α] [inst : IsRightCancelMulZero α] :
NoZeroDivisors α
source
ink
instance NoZeroDivisors.to_isCancelMulZero (α : Type u_1) [inst : Ring α] [inst : NoZeroDivisors α] :
IsCancelMulZero α
Equations
source
ink
theorem NoZeroDivisors.to_isDomain (α : Type u_1) [inst : Ring α] [h : Nontrivial α] [inst : NoZeroDivisors α] :
IsDomain α
source
ink
instance IsDomain.to_noZeroDivisors (α : Type u_1) [inst : Ring α] [inst : IsDomain α] :
NoZeroDivisors α
Equations