mathlib3 documentation

algebra.ring.basic

Semirings and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 add_hom.mul_left {R : Type u_1} [distrib R] (r : R) :
add_hom R R

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

Equations
source
@[simp]
theorem add_hom.mul_left_apply {R : Type u_1} [distrib R] (r : R) :
⇑(add_hom.mul_left r) = has_mul.mul r
source
@[simp]
theorem add_hom.mul_right_apply {R : Type u_1} [distrib R] (r : R) :
⇑(add_hom.mul_right r) = λ (a : R), a * r
source
def add_hom.mul_right {R : Type u_1} [distrib R] (r : R) :
add_hom R R

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

Equations
source
@[simp]
theorem map_bit0 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [add_hom_class F α β] (f : F) (a : α) :
⇑f (bit0 a) = bit0 (⇑f a)

Additive homomorphisms preserve bit0.

source
def add_monoid_hom.mul_left {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
R →+ R

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

Equations
source
@[simp]
theorem add_monoid_hom.coe_mul_left {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
⇑(add_monoid_hom.mul_left r) = has_mul.mul r
source
def add_monoid_hom.mul_right {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
R →+ R

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

Equations
source
@[simp]
theorem add_monoid_hom.coe_mul_right {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
⇑(add_monoid_hom.mul_right r) = λ (_x : R), _x * r
source
theorem add_monoid_hom.mul_right_apply {R : Type u_1} [non_unital_non_assoc_semiring R] (a r : R) :
⇑(add_monoid_hom.mul_right r) a = a * r
source
@[protected, instance]
def mul_opposite.has_distrib_neg {α : Type u} [has_mul α] [has_distrib_neg α] :
has_distrib_neg αᵐᵒᵖ
Equations
source
@[simp]
theorem inv_neg' {α : Type u} [group α] [has_distrib_neg α] (a : α) :
(-a)⁻¹ = -a⁻¹
source
theorem Vieta_formula_quadratic {α : Type u} [non_unital_comm_ring α] {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
theorem succ_ne_self {α : Type u} [non_assoc_ring α] [nontrivial α] (a : α) :
a + 1 ≠ a
source
theorem pred_ne_self {α : Type u} [non_assoc_ring α] [nontrivial α] (a : α) :
a - 1 ≠ a
source
theorem is_left_cancel_mul_zero.to_no_zero_divisors (α : Type u) [ring α] [is_left_cancel_mul_zero α] :
no_zero_divisors α
source
theorem is_right_cancel_mul_zero.to_no_zero_divisors (α : Type u) [ring α] [is_right_cancel_mul_zero α] :
no_zero_divisors α
source
@[protected, instance]
def no_zero_divisors.to_is_cancel_mul_zero (α : Type u) [ring α] [no_zero_divisors α] :
is_cancel_mul_zero α
source
theorem no_zero_divisors.to_is_domain (α : Type u) [ring α] [h : nontrivial α] [no_zero_divisors α] :
is_domain α
source
@[protected, instance]
def is_domain.to_no_zero_divisors (α : Type u) [ring α] [is_domain α] :
no_zero_divisors α