# mathlibdocumentation

algebra.ring.basic

# Properties and homomorphisms of semirings and rings #

This file proves simple properties of semirings, rings and domains and their unit groups. It also defines bundled homomorphisms of semirings and rings. As with monoid and groups, we use the same structure ring_hom a β, a.k.a. α →+* β, for both homomorphism types.

The unbundled homomorphisms are defined in deprecated/ring. They are deprecated and the plan is to slowly remove them from mathlib.

## Main definitions #

ring_hom, nonzero, domain, integral_domain

## Notations #

→+* for bundled ring homs (also use for semiring homs)

## Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no semiring_hom -- the idea is that ring_hom is used. The constructor for a ring_hom between semirings needs a proof of map_zero, map_one and map_add as well as map_mul; a separate constructor ring_hom.mk' will construct ring homs between rings from monoid homs given only a proof that addition is preserved.

## Tags #

ring_hom, semiring_hom, semiring, comm_semiring, ring, comm_ring, domain, integral_domain, nonzero, units

### distrib class #

@[instance]
def distrib.to_has_mul (R : Type u_1) [s : distrib R] :
@[class]
structure distrib (R : Type u_1) :
Type u_1
• mul : R → R → R
• add : R → R → R
• left_distrib : ∀ (a b c_1 : R), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : R), (a + b) * c_1 = a * c_1 + b * c_1

A typeclass stating that multiplication is left and right distributive over addition.

Instances
@[instance]
def distrib.to_has_add (R : Type u_1) [s : distrib R] :
theorem left_distrib {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c
theorem mul_add {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

theorem right_distrib {R : Type x} [distrib R] (a b c : R) :
(a + b) * c = a * c + b * c
theorem add_mul {R : Type x} [distrib R] (a b c : R) :
(a + b) * c = a * c + b * c

Alias of right_distrib.

def function.injective.distrib {R : Type x} {S : Type u_1} [has_mul R] [has_add R] [distrib S] (f : R → S) (hf : function.injective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = (f x) * f y) :

Pullback a distrib instance along an injective function.

Equations
def function.surjective.distrib {R : Type x} {S : Type u_1} [distrib R] [has_add S] [has_mul S] (f : R → S) (hf : function.surjective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = (f x) * f y) :

Pushforward a distrib instance along a surjective function.

Equations

### Semirings #

@[instance]
def semiring.to_add_comm_monoid (α : Type u) [s : semiring α] :
@[instance]
def semiring.to_distrib (α : Type u) [s : semiring α] :
@[class]
structure semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + x) . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * x) . "try_refl_tac"
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1

A semiring is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative monoid (monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class). The actual definition extends monoid_with_zero instead of monoid and mul_zero_class.

Instances
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [s : semiring α] :
def function.injective.semiring {α : Type u} {β : Type v} [semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback a semiring instance along an injective function.

Equations
def function.surjective.semiring {α : Type u} {β : Type v} [semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) :

Pushforward a semiring instance along a surjective function.

Equations
theorem one_add_one_eq_two {α : Type u} [semiring α] :
1 + 1 = 2
theorem two_mul {α : Type u} [semiring α] (n : α) :
2 * n = n + n
theorem distrib_three_right {α : Type u} [semiring α] (a b c d : α) :
(a + b + c) * d = a * d + b * d + c * d
theorem mul_two {α : Type u} [semiring α] (n : α) :
n * 2 = n + n
theorem bit0_eq_two_mul {α : Type u} [semiring α] (n : α) :
bit0 n = 2 * n
theorem add_ite {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
a + ite P b c = ite P (a + b) (a + c)
@[simp]
theorem mul_ite {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
a * ite P b c = ite P (a * b) (a * c)
theorem ite_add {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
ite P a b + c = ite P (a + c) (b + c)
@[simp]
theorem ite_mul {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
(ite P a b) * c = ite P (a * c) (b * c)
@[simp]
theorem mul_boole {α : Type u_1} [semiring α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
@[simp]
theorem boole_mul {α : Type u_1} [semiring α] (P : Prop) [decidable P] (a : α) :
(ite P 1 0) * a = ite P a 0
theorem ite_mul_zero_left {α : Type u_1} (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = (ite P a 0) * b
theorem ite_mul_zero_right {α : Type u_1} (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = a * ite P b 0
def even {α : Type u} [semiring α] (a : α) :
Prop

An element a of a semiring is even if there exists k such a = 2*k.

Equations
theorem even_iff_two_dvd {α : Type u} [semiring α] {a : α} :
even a 2 a
@[simp]
theorem range_two_mul (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x) = {a : α | even a}
@[simp]
theorem even_bit0 {α : Type u} [semiring α] (a : α) :
def odd {α : Type u} [semiring α] (a : α) :
Prop

An element a of a semiring is odd if there exists k such a = 2*k + 1.

Equations
• odd a = ∃ (k : α), a = 2 * k + 1
@[simp]
theorem odd_bit1 {α : Type u} [semiring α] (a : α) :
odd (bit1 a)
@[simp]
theorem range_two_mul_add_one (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x + 1) = {a : α | odd a}
theorem dvd_add {α : Type u} [semiring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
def add_monoid_hom.mul_left {R : Type u_1} [semiring R] (r : R) :
R →+ R

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

Equations
@[simp]
theorem add_monoid_hom.coe_mul_left {R : Type u_1} [semiring R] (r : R) :
def add_monoid_hom.mul_right {R : Type u_1} [semiring R] (r : R) :
R →+ R

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

Equations
@[simp]
theorem add_monoid_hom.coe_mul_right {R : Type u_1} [semiring R] (r : R) :
= λ (_x : R), _x * r
theorem add_monoid_hom.mul_right_apply {R : Type u_1} [semiring R] (a r : R) :
= a * r
def ring_hom.to_add_monoid_hom {α : Type u_1} {β : Type u_2} [semiring α] [semiring β] (s : α →+* β) :
α →+ β

Reinterpret a ring homomorphism f : R →+* S as an additive monoid homomorphism R →+ S. The simp-normal form is (f : R →+ S).

def ring_hom.to_monoid_hom {α : Type u_1} {β : Type u_2} [semiring α] [semiring β] (s : α →+* β) :
α →* β

Reinterpret a ring homomorphism f : R →+* S as a monoid homomorphism R →* S. The simp-normal form is (f : R →* S).

structure ring_hom (α : Type u_1) (β : Type u_2) [semiring α] [semiring β] :
Type (max u_1 u_2)

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both monoid_hom and monoid_with_zero_hom in order to put the fields in a sensible order, even though monoid_with_zero_hom already extends monoid_hom.

def ring_hom.to_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [semiring α] [semiring β] (s : α →+* β) :

Reinterpret a ring homomorphism f : R →+* S as a monoid_with_zero_hom R S. The simp-normal form is (f : monoid_with_zero_hom R S).

Throughout this section, some semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

@[instance]
def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
Equations
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
@[instance]
def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
has_coe →+* β) →* β)
Equations
@[simp]
theorem ring_hom.coe_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_monoid_hom_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_one' := h₁, map_mul' := h₂}
@[instance]
def ring_hom.has_coe_add_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
has_coe →+* β) →+ β)
Equations
@[simp]
theorem ring_hom.coe_add_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_add_monoid_hom_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_zero' := h₃, map_add' := h₄}
theorem ring_hom.congr_fun {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} {f g : α →+* β} (h : f = g) (x : α) :
f x = g x
theorem ring_hom.congr_arg {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) {x y : α} (h : x = y) :
f x = f y
theorem ring_hom.coe_inj {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} ⦃f g : α →+* β⦄ (h : f = g) :
f = g
@[ext]
theorem ring_hom.ext {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} ⦃f g : α →+* β⦄ (h : ∀ (x : α), f x = g x) :
f = g
theorem ring_hom.ext_iff {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} {f g : α →+* β} :
f = g ∀ (x : α), f x = g x
@[simp]
theorem ring_hom.mk_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
theorem ring_hom.coe_add_monoid_hom_injective {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
theorem ring_hom.coe_monoid_hom_injective {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
@[simp]
theorem ring_hom.map_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
f 0 = 0

Ring homomorphisms map zero to zero.

@[simp]
theorem ring_hom.map_one {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
f 1 = 1

Ring homomorphisms map one to one.

@[simp]
theorem ring_hom.map_add {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a b : α) :
f (a + b) = f a + f b

Ring homomorphisms preserve addition.

@[simp]
theorem ring_hom.map_mul {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a b : α) :
f (a * b) = (f a) * f b

Ring homomorphisms preserve multiplication.

@[simp]
theorem ring_hom.map_bit0 {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a : α) :
f (bit0 a) = bit0 (f a)

Ring homomorphisms preserve bit0.

@[simp]
theorem ring_hom.map_bit1 {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve bit1.

theorem ring_hom.codomain_trivial_iff_map_one_eq_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
0 = 1 f 1 = 0

f : R →+* S has a trivial codomain iff f 1 = 0.

theorem ring_hom.codomain_trivial_iff_range_trivial {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
0 = 1 ∀ (x : α), f x = 0

f : R →+* S has a trivial codomain iff it has a trivial range.

theorem ring_hom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
0 = 1 = {0}

f : R →+* S has a trivial codomain iff its range is {0}.

theorem ring_hom.map_one_ne_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) [nontrivial β] :
f 1 0

f : R →+* S doesn't map 1 to 0 if S is nontrivial

theorem ring_hom.domain_nontrivial {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) [nontrivial β] :

If there is a homomorphism f : R →+* S and S is nontrivial, then R is nontrivial.

theorem ring_hom.is_unit_map {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) {a : α} (h : is_unit a) :
def ring_hom.id (α : Type u_1) [semiring α] :
α →+* α

The identity ring homomorphism from a semiring to itself.

Equations
@[instance]
def ring_hom.inhabited {α : Type u} [rα : semiring α] :
Equations
@[simp]
theorem ring_hom.id_apply {α : Type u} [rα : semiring α] (x : α) :
(ring_hom.id α) x = x
def ring_hom.comp {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations
theorem ring_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {δ : Type u_1} {rδ : semiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of semiring homomorphisms is associative.

@[simp]
theorem ring_hom.coe_comp {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
(hnp.comp hmn) = hnp hmn
theorem ring_hom.comp_apply {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
(hnp.comp hmn) x = hnp (hmn x)
@[simp]
theorem ring_hom.comp_id {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :
f.comp (ring_hom.id α) = f
@[simp]
theorem ring_hom.id_comp {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :
(ring_hom.id β).comp f = f
@[instance]
def ring_hom.monoid {α : Type u} [rα : semiring α] :
monoid →+* α)
Equations
theorem ring_hom.one_def {α : Type u} [rα : semiring α] :
1 =
@[simp]
theorem ring_hom.coe_one {α : Type u} [rα : semiring α] :
theorem ring_hom.mul_def {α : Type u} [rα : semiring α] (f g : α →+* α) :
f * g = f.comp g
@[simp]
theorem ring_hom.coe_mul {α : Type u} [rα : semiring α] (f g : α →+* α) :
f * g = f g
theorem ring_hom.cancel_right {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem ring_hom.cancel_left {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[class]
structure comm_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
• mul_comm : ∀ (a b : α), a * b = b * a

A commutative semiring is a semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative commutative monoid (comm_monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances
@[instance]
def comm_semiring.to_comm_monoid (α : Type u) [s : comm_semiring α] :
@[instance]
def comm_semiring.to_semiring (α : Type u) [s : comm_semiring α] :
@[instance]
Equations
def function.injective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (f : γ → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : γ), f (x + y) = f x + f y) (mul : ∀ (x y : γ), f (x * y) = (f x) * f y) :

Pullback a semiring instance along an injective function.

Equations
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (f : α → γ) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) :

Pullback a semiring instance along an injective function.

Equations
theorem add_mul_self_eq {α : Type u} (a b : α) :
(a + b) * (a + b) = a * a + (2 * a) * b + b * b
@[simp]
theorem two_dvd_bit0 {α : Type u} {a : α} :
2 bit0 a
theorem ring_hom.map_dvd {α : Type u} {β : Type v} (f : α →+* β) {a b : α} :
a bf a f b

### Rings #

@[instance]
def ring.to_add_comm_group (α : Type u) [s : ring α] :
@[instance]
def ring.to_monoid (α : Type u) [s : ring α] :
@[class]
structure ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), x = x + x) . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), x = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1

A ring is a type with the following structures: additive commutative group (add_comm_group), multiplicative monoid (monoid), and distributive laws (distrib). Equivalently, a ring is a semiring with a negation operation making it an additive group.

Instances
@[instance]
def ring.to_distrib (α : Type u) [s : ring α] :
@[instance]
def ring.to_semiring {α : Type u} [ring α] :
Equations
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :
ring β

Pullback a ring instance along an injective function.

Equations
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) :
ring β

Pullback a ring instance along an injective function.

Equations
theorem neg_mul_eq_neg_mul {α : Type u} [ring α] (a b : α) :
-a * b = (-a) * b
theorem neg_mul_eq_mul_neg {α : Type u} [ring α] (a b : α) :
-a * b = a * -b
@[simp]
theorem neg_mul_eq_neg_mul_symm {α : Type u} [ring α] (a b : α) :
(-a) * b = -a * b
@[simp]
theorem mul_neg_eq_neg_mul_symm {α : Type u} [ring α] (a b : α) :
a * -b = -a * b
theorem neg_mul_neg {α : Type u} [ring α] (a b : α) :
(-a) * -b = a * b
theorem neg_mul_comm {α : Type u} [ring α] (a b : α) :
(-a) * b = a * -b
theorem neg_eq_neg_one_mul {α : Type u} [ring α] (a : α) :
-a = (-1) * a
theorem mul_sub_left_distrib {α : Type u} [ring α] (a b c : α) :
a * (b - c) = a * b - a * c
theorem mul_sub {α : Type u} [ring α] (a b c : α) :
a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

theorem mul_sub_right_distrib {α : Type u} [ring α] (a b c : α) :
(a - b) * c = a * c - b * c
theorem sub_mul {α : Type u} [ring α] (a b c : α) :
(a - b) * c = a * c - b * c

Alias of mul_sub_right_distrib.

theorem mul_neg_one {α : Type u} [ring α] (a : α) :
a * -1 = -a

An element of a ring multiplied by the additive inverse of one is the element's additive inverse.

theorem neg_one_mul {α : Type u} [ring α] (a : α) :
(-1) * a = -a

The additive inverse of one multiplied by an element of a ring is the element's additive inverse.

theorem mul_add_eq_mul_add_iff_sub_mul_add_eq {α : Type u} [ring α] {a b c d e : α} :
a * e + c = b * e + d (a - b) * e + c = d

An iff statement following from right distributivity in rings and the definition of subtraction.

theorem sub_mul_add_eq_of_mul_add_eq_mul_add {α : Type u} [ring α] {a b c d e : α} :
a * e + c = b * e + d(a - b) * e + c = d

A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.

@[instance]
def units.has_neg {α : Type u} [ring α] :

Each element of the group of units of a ring has an additive inverse.

Equations
@[simp]
theorem units.coe_neg {α : Type u} [ring α] (u : units α) :

Representing an element of a ring's unit group as an element of the ring commutes with mapping this element to its additive inverse.

@[simp]
theorem units.coe_neg_one {α : Type u} [ring α] :
-1 = -1
@[simp]
theorem units.neg_inv {α : Type u} [ring α] (u : units α) :

Mapping an element of a ring's unit group to its inverse commutes with mapping this element to its additive inverse.

@[simp]
theorem units.neg_neg {α : Type u} [ring α] (u : units α) :
--u = u

An element of a ring's unit group equals the additive inverse of its additive inverse.

@[simp]
theorem units.neg_mul {α : Type u} [ring α] (u₁ u₂ : units α) :
(-u₁) * u₂ = -u₁ * u₂

Multiplication of elements of a ring's unit group commutes with mapping the first argument to its additive inverse.

@[simp]
theorem units.mul_neg {α : Type u} [ring α] (u₁ u₂ : units α) :
u₁ * -u₂ = -u₁ * u₂

Multiplication of elements of a ring's unit group commutes with mapping the second argument to its additive inverse.

@[simp]
theorem units.neg_mul_neg {α : Type u} [ring α] (u₁ u₂ : units α) :
(-u₁) * -u₂ = u₁ * u₂

Multiplication of the additive inverses of two elements of a ring's unit group equals multiplication of the two original elements.

theorem units.neg_eq_neg_one_mul {α : Type u} [ring α] (u : units α) :
-u = (-1) * u

The additive inverse of an element of a ring's unit group equals the additive inverse of one times the original element.

theorem is_unit.neg {α : Type u} [ring α] {a : α} :
is_unit (-a)
@[simp]
theorem ring_hom.map_neg {α : Type u_1} {β : Type u_2} [ring α] [ring β] (f : α →+* β) (x : α) :
f (-x) = -f x

Ring homomorphisms preserve additive inverse.

@[simp]
theorem ring_hom.map_sub {α : Type u_1} {β : Type u_2} [ring α] [ring β] (f : α →+* β) (x y : α) :
f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

theorem ring_hom.injective_iff {α : Type u_1} {β : Type u_2} [ring α] [semiring β] (f : α →+* β) :
∀ (a : α), f a = 0a = 0

A ring homomorphism is injective iff its kernel is trivial.

def ring_hom.mk' {α : Type u} {γ : Type u_1} [semiring α] [ring γ] (f : α →* γ) (map_add : ∀ (a b : α), f (a + b) = f a + f b) :
α →+* γ

Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.

Equations
@[instance]
def comm_ring.to_ring (α : Type u) [s : comm_ring α] :
ring α
@[class]
structure comm_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + x) . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
• mul_comm : ∀ (a b : α), a * b = b * a

A commutative ring is a ring with commutative multiplication.

Instances
@[instance]
def comm_ring.to_comm_monoid (α : Type u) [s : comm_ring α] :
@[instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :
Equations
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback a comm_ring instance along an injective function.

Equations
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) :

Pullback a comm_ring instance along an injective function.

Equations
theorem dvd_neg_of_dvd {α : Type u} [comm_ring α] {a b : α} (h : a b) :
a -b
theorem dvd_of_dvd_neg {α : Type u} [comm_ring α] {a b : α} (h : a -b) :
a b
theorem dvd_neg_iff_dvd {α : Type u} [comm_ring α] (a b : α) :
a -b a b
theorem neg_dvd_of_dvd {α : Type u} [comm_ring α] {a b : α} (h : a b) :
-a b
theorem dvd_of_neg_dvd {α : Type u} [comm_ring α] {a b : α} (h : -a b) :
a b
theorem neg_dvd_iff_dvd {α : Type u} [comm_ring α] (a b : α) :
-a b a b
theorem dvd_sub {α : Type u} [comm_ring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u} [comm_ring α] {a b c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u} [comm_ring α] {a b c : α} (h : a b) :
a c a b + c
theorem two_dvd_bit1 {α : Type u} [comm_ring α] {a : α} :
2 bit1 a 2 1
theorem mul_self_sub_mul_self {α : Type u} [comm_ring α] (a b : α) :
a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares in a commutative ring as a product.

theorem mul_self_sub_one {α : Type u} [comm_ring α] (a : α) :
a * a - 1 = (a + 1) * (a - 1)
@[simp]
theorem dvd_neg {α : Type u} [comm_ring α] (a b : α) :
a -b a b

An element a of a commutative ring divides the additive inverse of an element b iff a divides b.

@[simp]
theorem neg_dvd {α : Type u} [comm_ring α] (a b : α) :
-a b a b

The additive inverse of an element a of a commutative ring divides another element b iff a divides b.

theorem dvd_add_left {α : Type u} [comm_ring α] {a b c : α} (h : a c) :
a b + c a b

If an element a divides another element c in a commutative ring, a divides the sum of another element b with c iff a divides b.

theorem dvd_add_right {α : Type u} [comm_ring α] {a b c : α} (h : a b) :
a b + c a c

If an element a divides another element b in a commutative ring, a divides the sum of b and another element c iff a divides c.

@[simp]
theorem dvd_add_self_left {α : Type u} [comm_ring α] {a b : α} :
a a + b a b

An element a divides the sum a + b if and only if a divides b.

@[simp]
theorem dvd_add_self_right {α : Type u} [comm_ring α] {a b : α} :
a b + a a b

An element a divides the sum b + a if and only if a divides b.

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

theorem dvd_mul_sub_mul {α : Type u} [comm_ring α] {k a b x y : α} (hab : k a - b) (hxy : k x - y) :
k a * x - b * y
theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [comm_ring α] {a b c : α} (h : a b - c) :
a b a c
theorem succ_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a + 1 a
theorem pred_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a - 1 a
@[instance]
def domain.to_ring (α : Type u) [s : domain α] :
ring α
@[class]
structure domain (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), x = x + x) . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), x = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
• exists_pair_ne : ∃ (x y : α), x y
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0

A domain is a ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0. Alternatively, a domain is an integral domain without assuming commutativity of multiplication.

Instances
@[instance]
def domain.to_nontrivial (α : Type u) [s : domain α] :
@[instance]
def domain.to_no_zero_divisors {α : Type u} [domain α] :
@[instance]
def domain.to_cancel_monoid_with_zero {α : Type u} [domain α] :
Equations
def function.injective.domain {α : Type u} {β : Type v} [domain α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback a domain instance along an injective function.

Equations

### Integral domains #

@[class]
structure integral_domain (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
• mul_comm : ∀ (a b : α), a * b = b * a
• exists_pair_ne : ∃ (x y : α), x y
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0

An integral domain is a commutative ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0. Alternatively, an integral domain is a domain with commutative multiplication.

Instances
@[instance]
def integral_domain.to_domain (α : Type u) [s : integral_domain α] :
@[instance]
def integral_domain.to_comm_ring (α : Type u) [s : integral_domain α] :
@[instance]
Equations
def function.injective.integral_domain {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback an integral_domain instance along an injective function.

Equations
theorem mul_self_eq_mul_self_iff {α : Type u} {a b : α} :
a * a = b * b a = b a = -b
theorem mul_self_eq_one_iff {α : Type u} {a : α} :
a * a = 1 a = 1 a = -1
theorem units.inv_eq_self_iff {α : Type u} (u : units α) :
u⁻¹ = u u = 1 u = -1

In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.

def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
β →+* α

Makes a ring homomorphism from an additive group homomorphism from a commutative ring to an integral domain that commutes with self multiplication, assumes that two is nonzero and one is sent to one.

Equations
@[simp]
theorem add_monoid_hom.coe_fn_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
h_two h_one) = f
@[simp]
theorem add_monoid_hom.coe_add_monoid_hom_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
h_two h_one) = f
def ring.inverse {M₀ : Type u_1} [monoid_with_zero M₀] :
M₀ → M₀

Introduce a function inverse on a monoid with zero M₀, which sends x to x⁻¹ if x is invertible and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the ring namespace for brevity, it requires the weaker assumption monoid_with_zero M₀ instead of ring M₀.

Equations
@[simp]
theorem ring.inverse_unit {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) :

By definition, if x is invertible then inverse x = x⁻¹.

@[simp]
theorem ring.inverse_non_unit {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : ¬) :

By definition, if x is not invertible then inverse x = 0.

@[nolint]
def is_integral_domain.to_nontrivial {R : Type u} [ring R] (s : is_integral_domain R) :
structure is_integral_domain (R : Type u) [ring R] :
Prop
• exists_pair_ne : ∃ (x y : R), x y
• mul_comm : ∀ (x y : R), x * y = y * x
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (x y : R), x * y = 0x = 0 y = 0

A predicate to express that a ring is an integral domain.

This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms.

theorem integral_domain.to_is_integral_domain (R : Type u)  :

Every integral domain satisfies the predicate for integral domains.

If a ring satisfies the predicate for integral domains, then it can be endowed with an integral_domain instance whose data is definitionally equal to the existing data.

Equations
@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} (h : x y) (h' : x' y') :
(x + x') (y + y')
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a + b) x y
theorem semiconj_by.neg_right {R : Type x} [ring R] {a x y : R} (h : x y) :
(-x) (-y)
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [ring R] {a x y : R} :
(-x) (-y) x y
theorem semiconj_by.neg_left {R : Type x} [ring R] {a x y : R} (h : x y) :
semiconj_by (-a) x y
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [ring R] {a x y : R} :
semiconj_by (-a) x y x y
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [ring R] (a : R) :
(-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [ring R] (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} [ring R] {a x y x' y' : R} (h : x y) (h' : x' y') :
(x - x') (y - y')
@[simp]
theorem semiconj_by.sub_left {R : Type x} [ring R] {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a - b) x y
@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
b c (b + c)
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
c ccommute (a + b) c
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : y) :
(bit0 y)
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : y) :
theorem commute.bit1_right {R : Type x} [semiring R] {x y : R} (h : y) :
(bit1 y)
theorem commute.bit1_left {R : Type x} [semiring R] {x y : R} (h : y) :
theorem commute.neg_right {R : Type x} [ring R] {a b : R} :
b (-b)
@[simp]
theorem commute.neg_right_iff {R : Type x} [ring R] {a b : R} :
(-b) b
theorem commute.neg_left {R : Type x} [ring R] {a b : R} :
bcommute (-a) b
@[simp]
theorem commute.neg_left_iff {R : Type x} [ring R] {a b : R} :
commute (-a) b b
@[simp]
theorem commute.neg_one_right {R : Type x} [ring R] (a : R) :
(-1)
@[simp]
theorem commute.neg_one_left {R : Type x} [ring R] (a : R) :
commute (-1) a
@[simp]
theorem commute.sub_right {R : Type x} [ring R] {a b c : R} :
b c (b - c)
@[simp]
theorem commute.sub_left {R : Type x} [ring R] {a b c : R} :
c ccommute (a - b) c