mathlib documentation

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, is_domain

Notations #

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

Implementation notes #

Tags #

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

distrib class #

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

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

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

Alias of left_distrib.

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

Alias of right_distrib.

source
theorem distrib_three_right {R : Type x} [distrib R] (a b c d : R) :
(a + b + c) * d = a * d + b * d + c * d
source
@[protected]
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) :
distrib R

Pullback a distrib instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
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) :
distrib S

Pushforward a distrib instance along a surjective function. See note [reducible non-instances].

Equations

Semirings #

source
@[instance]
def non_unital_non_assoc_semiring.to_distrib (α : Type u) [self : non_unital_non_assoc_semiring α] :
distrib α
source
@[instance]
def non_unital_non_assoc_semiring.to_mul_zero_class (α : Type u) [self : non_unital_non_assoc_semiring α] :
mul_zero_class α
source
@[instance]
def non_unital_non_assoc_semiring.to_add_comm_monoid (α : Type u) [self : non_unital_non_assoc_semiring α] :
add_comm_monoid α
source
@[class]
structure non_unital_non_assoc_semiring (α : Type u) :
Type u

A not-necessarily-unital, not-necessarily-associative semiring.

Instances
source
@[instance]
def non_unital_semiring.to_semigroup_with_zero (α : Type u) [self : non_unital_semiring α] :
semigroup_with_zero α
source
@[instance]
def non_unital_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_semiring α] :
non_unital_non_assoc_semiring α
source
@[class]
structure non_unital_semiring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), non_unital_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_semiring.nsmul n.succ x = x + non_unital_semiring.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c

An associative but not-necessarily unital semiring.

Instances
source
@[instance]
def non_assoc_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_assoc_semiring α] :
non_unital_non_assoc_semiring α
source
@[instance]
def non_assoc_semiring.to_mul_zero_one_class (α : Type u) [self : non_assoc_semiring α] :
mul_zero_one_class α
source
@[class]
structure non_assoc_semiring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), non_assoc_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), non_assoc_semiring.nsmul n.succ x = x + non_assoc_semiring.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a

A unital but not-necessarily-associative semiring.

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

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
source
@[instance]
def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :
non_unital_semiring α
source
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :
monoid_with_zero α
source
@[protected]
def function.injective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_unital_non_assoc_semiring α] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
non_unital_non_assoc_semiring β

Pullback a non_unital_non_assoc_semiring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_unital_semiring α] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
non_unital_semiring β

Pullback a non_unital_semiring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_assoc_semiring α] [has_one β] (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
non_assoc_semiring β

Pullback a non_assoc_semiring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [semiring α] [has_one β] [has_pow β ℕ] (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
semiring β

Pullback a semiring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_unital_non_assoc_semiring α] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) :
non_unital_non_assoc_semiring β

Pushforward a non_unital_non_assoc_semiring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_unital_semiring α] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = (f x) * f y) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) :
non_unital_semiring β

Pushforward a non_unital_semiring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [non_assoc_semiring α] [has_one β] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) :
non_assoc_semiring β

Pushforward a non_assoc_semiring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_scalar ℕ β] {α : Type u} [semiring α] [has_one β] [has_pow β ℕ] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) :
semiring β

Pushforward a semiring instance along a surjective function. See note [reducible non-instances].

Equations
source
theorem dvd_add {α : Type u} [non_unital_semiring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b + c
source
theorem add_one_mul {α : Type u} [non_assoc_semiring α] (a b : α) :
(a + 1) * b = a * b + b
source
theorem mul_add_one {α : Type u} [non_assoc_semiring α] (a b : α) :
a * (b + 1) = a * b + a
source
theorem one_add_mul {α : Type u} [non_assoc_semiring α] (a b : α) :
(1 + a) * b = b + a * b
source
theorem mul_one_add {α : Type u} [non_assoc_semiring α] (a b : α) :
a * (1 + b) = a + a * b
source
theorem two_mul {α : Type u} [non_assoc_semiring α] (n : α) :
2 * n = n + n
source
theorem mul_two {α : Type u} [non_assoc_semiring α] (n : α) :
n * 2 = n + n
source
theorem one_add_one_eq_two {α : Type u} [semiring α] :
1 + 1 = 2
source
theorem bit0_eq_two_mul {α : Type u} [semiring α] (n : α) :
bit0 n = 2 * n
source
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)
source
@[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)
source
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)
source
@[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)
source
@[simp]
theorem mul_boole {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
source
@[simp]
theorem boole_mul {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :
(ite P 1 0) * a = ite P a 0
source
theorem ite_mul_zero_left {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = (ite P a 0) * b
source
theorem ite_mul_zero_right {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = a * ite P b 0
source
theorem ite_and_mul_zero {α : Type u_1} [mul_zero_class α] (P Q : Prop) [decidable P] [decidable Q] (a b : α) :
ite (P ∧ Q) (a * b) 0 = (ite P a 0) * ite Q b 0
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
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
def ring_hom.to_add_monoid_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :
α →+ β

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

source
def ring_hom.to_monoid_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :
α →* β

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

source
structure ring_hom (α : Type u_1) (β : Type u_2) [non_assoc_semiring α] [non_assoc_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.

source
def ring_hom.to_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :
α →*₀ β

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

source
@[instance]
def ring_hom_class.to_monoid_with_zero_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
monoid_with_zero_hom_class F R S
source
@[instance]
def ring_hom_class.to_monoid_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
monoid_hom_class F R S
source
@[class]
structure ring_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] :
Type (max u_1 u_2 u_3)

ring_hom_class F R S states that F is a type of (semi)ring homomorphisms. You should extend this class when you extend ring_hom.

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

Instances
source
@[instance]
def ring_hom_class.to_add_monoid_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
add_monoid_hom_class F R S
source
@[simp]
theorem map_bit0 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] (f : F) (a : α) :
⇑f (bit0 a) = bit0 (⇑f a)

Ring homomorphisms preserve bit0.

source
@[simp]
theorem map_bit1 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] (f : F) (a : α) :
⇑f (bit1 a) = bit1 (⇑f a)

Ring homomorphisms preserve bit1.

source
@[protected, instance]
def ring_hom.has_coe_t {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] :
has_coe_t F (α →+* β)
Equations

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

source
@[protected, instance]
def ring_hom.ring_hom_class {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
ring_hom_class (α →+* β) α β
Equations
source
@[protected, instance]
def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe_to_fun (α →+* β) (λ (_x : α →+* β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_fun = ⇑f
source
@[simp]
theorem ring_hom.coe_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_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
source
@[simp]
theorem ring_hom.coe_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {F : Type u_1} [ring_hom_class F α β] (f : F) :
⇑↑f = ⇑f
source
@[protected, instance]
def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe (α →+* β) (α →* β)
Equations
source
@[simp, norm_cast]
theorem ring_hom.coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑↑f = ⇑f
source
@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_monoid_hom = ↑f
source
@[simp]
theorem ring_hom.to_monoid_with_zero_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑(f.to_monoid_with_zero_hom) = ⇑f
source
@[simp]
theorem ring_hom.coe_monoid_hom_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_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₂}
source
@[simp, norm_cast]
theorem ring_hom.coe_add_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑↑f = ⇑f
source
@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_add_monoid_hom = ↑f
source
@[simp]
theorem ring_hom.coe_add_monoid_hom_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_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₄}
source
def ring_hom.copy {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f) :
α →+* β

Copy of a ring_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
theorem ring_hom.congr_fun {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} (h : f = g) (x : α) :
⇑f x = ⇑g x
source
theorem ring_hom.congr_arg {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) {x y : α} (h : x = y) :
⇑f x = ⇑f y
source
theorem ring_hom.coe_inj {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : ⇑f = ⇑g) :
f = g
source
@[ext]
theorem ring_hom.ext {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
source
theorem ring_hom.ext_iff {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} :
f = g ↔ ∀ (x : α), ⇑f x = ⇑g x
source
@[simp]
theorem ring_hom.mk_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_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
source
theorem ring_hom.coe_add_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
function.injective coe
source
theorem ring_hom.coe_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
function.injective coe
source
@[protected]
theorem ring_hom.map_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑f 0 = 0

Ring homomorphisms map zero to zero.

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

Ring homomorphisms map one to one.

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

Ring homomorphisms preserve addition.

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

Ring homomorphisms preserve multiplication.

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

Ring homomorphisms preserve bit0.

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

Ring homomorphisms preserve bit1.

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

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

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

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

source
theorem ring_hom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 ↔ set.range ⇑f = {0}

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

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

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

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

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

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

The identity ring homomorphism from a semiring to itself.

Equations
source
@[protected, instance]
def ring_hom.inhabited {α : Type u} [rα : non_assoc_semiring α] :
inhabited (α →+* α)
Equations
source
@[simp]
theorem ring_hom.id_apply {α : Type u} [rα : non_assoc_semiring α] (x : α) :
⇑(ring_hom.id α) x = x
source
@[simp]
theorem ring_hom.coe_add_monoid_hom_id {α : Type u} [rα : non_assoc_semiring α] :
↑(ring_hom.id α) = add_monoid_hom.id α
source
@[simp]
theorem ring_hom.coe_monoid_hom_id {α : Type u} [rα : non_assoc_semiring α] :
↑(ring_hom.id α) = monoid_hom.id α
source
def ring_hom.comp {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

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

Composition of semiring homomorphisms is associative.

source
@[simp]
theorem ring_hom.coe_comp {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn
source
theorem ring_hom.comp_apply {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
⇑(hnp.comp hmn) x = ⇑hnp (⇑hmn x)
source
@[simp]
theorem ring_hom.comp_id {α : Type u} {β : Type v} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
f.comp (ring_hom.id α) = f
source
@[simp]
theorem ring_hom.id_comp {α : Type u} {β : Type v} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
(ring_hom.id β).comp f = f
source
@[protected, instance]
def ring_hom.monoid {α : Type u} [rα : non_assoc_semiring α] :
monoid (α →+* α)
Equations
source
theorem ring_hom.one_def {α : Type u} [rα : non_assoc_semiring α] :
1 = ring_hom.id α
source
@[simp]
theorem ring_hom.coe_one {α : Type u} [rα : non_assoc_semiring α] :
⇑1 = id
source
theorem ring_hom.mul_def {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
f * g = f.comp g
source
@[simp]
theorem ring_hom.coe_mul {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
⇑f * g = ⇑f ∘ ⇑g
source
theorem ring_hom.cancel_right {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
theorem ring_hom.cancel_left {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
@[simp]
theorem two_dvd_bit0 {α : Type u} [semiring α] {a : α} :
2 ∣ bit0 a
source
theorem ring_hom.map_dvd {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) {a b : α} :
a ∣ b → ⇑f a ∣ ⇑f b
source
@[class]
structure comm_semiring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), comm_semiring.nsmul n.succ x = x + comm_semiring.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), comm_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), comm_semiring.npow n.succ x = x * comm_semiring.npow n x) . "try_refl_tac"
  • 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
source
@[instance]
def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :
comm_monoid α
source
@[instance]
def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :
semiring α
source
@[protected, instance]
def comm_semiring.to_comm_monoid_with_zero {α : Type u} [comm_semiring α] :
comm_monoid_with_zero α
Equations
source
@[protected]
def function.injective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [has_scalar ℕ γ] [has_pow γ ℕ] (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) (nsmul : ∀ (x : γ) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : γ) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_semiring γ

Pullback a semiring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [has_scalar ℕ γ] [has_pow γ ℕ] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_semiring γ

Pushforward a semiring instance along a surjective function. See note [reducible non-instances].

Equations
source
theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :
(a + b) * (a + b) = a * a + (2 * a) * b + b * b
source
theorem has_dvd.dvd.linear_comb {α : Type u} [comm_semiring α] {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) :
d ∣ a * x + b * y
source
@[instance]
def has_distrib_neg.to_has_involutive_neg (α : Type u_1) [has_mul α] [self : has_distrib_neg α] :
has_involutive_neg α
source
@[class]
structure has_distrib_neg (α : Type u_1) [has_mul α] :
Type u_1
  • neg : α → α
  • neg_neg : ∀ (x : α), --x = x
  • neg_mul : ∀ (x y : α), (-x) * y = -x * y
  • mul_neg : ∀ (x y : α), x * -y = -x * y

Typeclass for a negation operator that distributes across multiplication.

This is useful for dealing with submonoids of a ring that contain -1 without having to duplicate lemmas.

Instances
source
@[simp]
theorem neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
(-a) * b = -a * b
source
@[simp]
theorem mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
a * -b = -a * b
source
theorem neg_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
(-a) * -b = a * b
source
theorem neg_mul_eq_neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = (-a) * b
source
theorem neg_mul_eq_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = a * -b
source
theorem neg_mul_comm {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
(-a) * b = a * -b
source
theorem neg_eq_neg_one_mul {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :
-a = (-1) * a
source
theorem mul_neg_one {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :
a * -1 = -a

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

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

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

source
@[simp]
theorem neg_zero' {α : Type u} [mul_zero_class α] [has_distrib_neg α] :
-0 = 0

Prefer neg_zero if add_comm_group is available.

source
@[simp]
theorem inv_neg' {α : Type u} [group α] [has_distrib_neg α] (a : α) :
(-a)⁻¹ = -a⁻¹

Rings #

source
@[instance]
def non_unital_non_assoc_ring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_non_assoc_ring α] :
non_unital_non_assoc_semiring α
source
@[class]
structure non_unital_non_assoc_ring (α : Type u) :
Type u

A not-necessarily-unital, not-necessarily-associative ring.

Instances
source
@[instance]
def non_unital_non_assoc_ring.to_add_comm_group (α : Type u) [self : non_unital_non_assoc_ring α] :
add_comm_group α
source
@[protected]
def function.injective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [non_unital_non_assoc_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
non_unital_non_assoc_ring β

Pullback a non_unital_non_assoc_ring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [non_unital_non_assoc_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) :
non_unital_non_assoc_ring β

Pushforward a non_unital_non_assoc_ring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[protected, instance]
def non_unital_non_assoc_ring.to_has_distrib_neg {α : Type u} [non_unital_non_assoc_ring α] :
has_distrib_neg α
Equations
source
theorem mul_sub_left_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
a * (b - c) = a * b - a * c
source
theorem mul_sub {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

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

Alias of mul_sub_right_distrib.

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

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

source
@[instance]
def non_unital_ring.to_non_unital_semiring (α : Type u_1) [self : non_unital_ring α] :
non_unital_semiring α
source
@[class]
structure non_unital_ring (α : Type u_1) :
Type u_1

An associative but not-necessarily unital ring.

Instances
source
@[instance]
def non_unital_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_unital_ring α] :
non_unital_non_assoc_ring α
source
@[protected]
def function.injective.non_unital_ring {α : Type u} {β : Type v} [non_unital_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
non_unital_ring β

Pullback a non_unital_ring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_unital_ring {α : Type u} {β : Type v} [non_unital_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) :
non_unital_ring β

Pushforward a non_unital_ring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[class]
structure non_assoc_ring (α : Type u_1) :
Type u_1

A unital but not-necessarily-associative ring.

Instances
source
@[instance]
def non_assoc_ring.to_non_assoc_semiring (α : Type u_1) [self : non_assoc_ring α] :
non_assoc_semiring α
source
@[instance]
def non_assoc_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_assoc_ring α] :
non_unital_non_assoc_ring α
source
@[protected]
def function.injective.non_assoc_ring {α : Type u} {β : Type v} [non_assoc_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
non_assoc_ring β

Pullback a non_assoc_ring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.non_assoc_ring {α : Type u} {β : Type v} [non_assoc_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) :
non_assoc_ring β

Pushforward a non_unital_ring instance along a surjective function. See note [reducible non-instances].

Equations
source
theorem sub_one_mul {α : Type u} [non_assoc_ring α] (a b : α) :
(a - 1) * b = a * b - b
source
theorem mul_sub_one {α : Type u} [non_assoc_ring α] (a b : α) :
a * (b - 1) = a * b - a
source
theorem one_sub_mul {α : Type u} [non_assoc_ring α] (a b : α) :
(1 - a) * b = b - a * b
source
theorem mul_one_sub {α : Type u} [non_assoc_ring α] (a b : α) :
a * (1 - b) = a - a * b
source
@[instance]
def ring.to_add_comm_group (α : Type u) [self : ring α] :
add_comm_group α
source
@[instance]
def ring.to_monoid (α : Type u) [self : ring α] :
monoid α
source
@[class]
structure ring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ring.nsmul n.succ x = x + ring.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • zsmul : ℤ → α → α
  • zsmul_zero' : (∀ (a : α), ring.zsmul 0 a = 0) . "try_refl_tac"
  • zsmul_succ' : (∀ (n : ℕ) (a : α), ring.zsmul (int.of_nat n.succ) a = a + ring.zsmul (int.of_nat n) a) . "try_refl_tac"
  • zsmul_neg' : (∀ (n : ℕ) (a : α), ring.zsmul -[1+ n] a = -ring.zsmul ↑(n.succ) a) . "try_refl_tac"
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ring.npow n.succ x = x * ring.npow n x) . "try_refl_tac"
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

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
source
@[instance]
def ring.to_distrib (α : Type u) [self : ring α] :
distrib α
source
@[protected, instance]
def ring.to_non_unital_ring {α : Type u} [ring α] :
non_unital_ring α
Equations
source
@[protected, instance]
def ring.to_non_assoc_ring {α : Type u} [ring α] :
non_assoc_ring α
Equations
source
@[protected, instance]
def ring.to_semiring {α : Type u} [ring α] :
semiring α
Equations
source
@[protected]
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ] (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
ring β

Pullback a ring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) :
ring β

Pushforward a ring instance along a surjective function. See note [reducible non-instances].

Equations
source
@[protected, instance]
def units.has_neg {α : Type u} [ring α] :
has_neg αˣ

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

Equations
source
@[protected, simp, norm_cast]
theorem units.coe_neg {α : Type u} [ring α] (u : αˣ) :
↑-u = -↑u

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

source
@[protected, simp, norm_cast]
theorem units.coe_neg_one {α : Type u} [ring α] :
↑-1 = -1
source
@[protected, instance]
def units.has_distrib_neg {α : Type u} [ring α] :
has_distrib_neg αˣ
Equations
source
theorem is_unit.neg {α : Type u} [ring α] {a : α} :
is_unit a → is_unit (-a)
source
theorem is_unit.neg_iff {α : Type u} [ring α] (a : α) :
is_unit (-a) ↔ is_unit a
source
theorem is_unit.sub_iff {α : Type u} [ring α] {x y : α} :
is_unit (x - y) ↔ is_unit (y - x)
source
@[protected]
theorem ring_hom.map_neg {α : Type u_1} {β : Type u_2} [non_assoc_ring α] [non_assoc_ring β] (f : α →+* β) (x : α) :
⇑f (-x) = -⇑f x

Ring homomorphisms preserve additive inverse.

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

Ring homomorphisms preserve subtraction.

source
def ring_hom.mk' {α : Type u} {γ : Type u_1} [non_assoc_semiring α] [non_assoc_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
source
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
source
@[class]
structure comm_ring (α : Type u) :
Type u

A commutative ring is a ring with commutative multiplication.

Instances
source
@[instance]
def comm_ring.to_comm_monoid (α : Type u) [self : comm_ring α] :
comm_monoid α
source
@[protected, instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :
comm_semiring α
Equations
source
theorem dvd_neg_of_dvd {α : Type u} [ring α] {a b : α} (h : a ∣ b) :
a ∣ -b
source
theorem dvd_of_dvd_neg {α : Type u} [ring α] {a b : α} (h : a ∣ -b) :
a ∣ b
source
@[simp]
theorem dvd_neg {α : Type u} [ring α] (a b : α) :
a ∣ -b ↔ a ∣ b

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

source
theorem neg_dvd_of_dvd {α : Type u} [ring α] {a b : α} (h : a ∣ b) :
-a ∣ b
source
theorem dvd_of_neg_dvd {α : Type u} [ring α] {a b : α} (h : -a ∣ b) :
a ∣ b
source
@[simp]
theorem neg_dvd {α : Type u} [ring α] (a b : α) :
-a ∣ b ↔ a ∣ b

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

source
theorem dvd_sub {α : Type u} [ring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b - c
source
theorem dvd_add_iff_left {α : Type u} [ring α] {a b c : α} (h : a ∣ c) :
a ∣ b ↔ a ∣ b + c
source
theorem dvd_add_iff_right {α : Type u} [ring α] {a b c : α} (h : a ∣ b) :
a ∣ c ↔ a ∣ b + c
source
theorem two_dvd_bit1 {α : Type u} [ring α] {a : α} :
2 ∣ bit1 a ↔ 2 ∣ 1
source
theorem dvd_add_left {α : Type u} [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.

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

source
@[simp]
theorem dvd_add_self_left {α : Type u} [ring α] {a b : α} :
a ∣ a + b ↔ a ∣ b

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

source
@[simp]
theorem dvd_add_self_right {α : Type u} [ring α] {a b : α} :
a ∣ b + a ↔ a ∣ b

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

source
theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [ring α] {a b c : α} (h : a ∣ b - c) :
a ∣ b ↔ a ∣ c
source
@[protected]
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ] (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) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_ring β

Pullback a comm_ring instance along an injective function. See note [reducible non-instances].

Equations
source
@[protected]
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] [has_pow β ℕ] (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) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_ring β

Pushforward a comm_ring instance along a surjective function. See note [reducible non-instances].

Equations
source
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.

source
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
source
theorem succ_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a + 1 ≠ a
source
theorem pred_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a - 1 ≠ a
source
theorem is_left_regular_of_non_zero_divisor {α : Type u} [non_unital_non_assoc_ring α] (k : α) (h : ∀ (x : α), k * x = 0 → x = 0) :
is_left_regular k

Left mul by a k : α over [ring α] is injective, if k is not a zero divisor. The typeclass that restricts all terms of α to have this property is no_zero_divisors.

source
theorem is_right_regular_of_non_zero_divisor {α : Type u} [non_unital_non_assoc_ring α] (k : α) (h : ∀ (x : α), x * k = 0 → x = 0) :
is_right_regular k

Right mul by a k : α over [ring α] is injective, if k is not a zero divisor. The typeclass that restricts all terms of α to have this property is no_zero_divisors.

source
theorem is_regular_of_ne_zero' {α : Type u} [ring α] [no_zero_divisors α] {k : α} (hk : k ≠ 0) :
is_regular k
source
theorem is_regular_iff_ne_zero' {α : Type u} [nontrivial α] [ring α] [no_zero_divisors α] {k : α} :
is_regular k ↔ k ≠ 0
source
def no_zero_divisors.to_cancel_monoid_with_zero {α : Type u} [ring α] [no_zero_divisors α] :
cancel_monoid_with_zero α

A ring with no zero divisors is a cancel_monoid_with_zero.

Note this is not an instance as it forms a typeclass loop.

Equations
source
@[instance]
def is_domain.to_no_zero_divisors (α : Type u) [ring α] [self : is_domain α] :
no_zero_divisors α
source
@[class]
structure is_domain (α : Type u) [ring α] :
Prop
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0 → a = 0 ∨ b = 0
  • exists_pair_ne : ∃ (x y : α), x ≠ y

A domain is a nontrivial ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0.

This is implemented as a mixin for ring α. To obtain an integral domain use [comm_ring α] [is_domain α].

Instances
source
@[instance]
def is_domain.to_nontrivial (α : Type u) [ring α] [self : is_domain α] :
nontrivial α
source
@[protected, instance]
def is_domain.to_cancel_monoid_with_zero {α : Type u} [ring α] [is_domain α] :
cancel_monoid_with_zero α
Equations
source
@[protected]
theorem function.injective.is_domain {α : Type u} {β : Type v} [ring α] [is_domain α] [ring β] (f : β →+* α) (hf : function.injective ⇑f) :
is_domain β

Pullback an is_domain instance along an injective function.

source
@[protected, instance]
def is_domain.to_cancel_comm_monoid_with_zero {α : Type u} [comm_ring α] [is_domain α] :
cancel_comm_monoid_with_zero α
Equations
source
def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring α] [is_domain α] [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
source
@[simp]
theorem add_monoid_hom.coe_fn_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), ⇑f (x * x) = (⇑f x) * ⇑f x) (h_two : 2 ≠ 0) (h_one : ⇑f 1 = 1) :
⇑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = ⇑f
source
@[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 α] [is_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), ⇑f (x * x) = (⇑f x) * ⇑f x) (h_two : 2 ≠ 0) (h_one : ⇑f 1 = 1) :
↑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = f
source
@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x + x') (y + y')
source
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a + b) x y
source
theorem semiconj_by.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by a (-x) (-y)
source
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
semiconj_by a (-x) (-y) ↔ semiconj_by a x y
source
theorem semiconj_by.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by (-a) x y
source
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
semiconj_by (-a) x y ↔ semiconj_by a x y
source
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
semiconj_by a (-1) (-1)
source
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (x : R) :
semiconj_by (-1) x x
source
@[simp]
theorem semiconj_by.sub_right {R : Type x} [ring R] {a x y x' y' : R} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x - x') (y - y')
source
@[simp]
theorem semiconj_by.sub_left {R : Type x} [ring R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a - b) x y
source
@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
commute a b → commute a c → commute a (b + c)
source
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
commute a c → commute b c → commute (a + b) c
source
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : commute x y) :
commute x (bit0 y)
source
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : commute x y) :
commute (bit0 x) y
source
theorem commute.bit1_right {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
commute x (bit1 y)
source
theorem commute.bit1_left {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
commute (bit1 x) y
source
theorem commute.mul_self_sub_mul_self_eq {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares of commuting elements as a product.

source
theorem commute.mul_self_sub_mul_self_eq' {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
a * a - b * b = (a - b) * (a + b)
source
theorem commute.mul_self_eq_mul_self_iff {R : Type x} [non_unital_non_assoc_ring R] [no_zero_divisors R] {a b : R} (h : commute a b) :
a * a = b * b ↔ a = b ∨ a = -b
source
theorem commute.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a b → commute a (-b)
source
@[simp]
theorem commute.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a (-b) ↔ commute a b
source
theorem commute.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a b → commute (-a) b
source
@[simp]
theorem commute.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute (-a) b ↔ commute a b
source
@[simp]
theorem commute.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute a (-1)
source
@[simp]
theorem commute.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute (-1) a
source
@[simp]
theorem commute.sub_right {R : Type x} [ring R] {a b c : R} :
commute a b → commute a c → commute a (b - c)
source
@[simp]
theorem commute.sub_left {R : Type x} [ring R] {a b c : R} :
commute a c → commute b c → commute (a - b) c
source
theorem mul_self_sub_mul_self {R : Type x} [comm_ring R] (a b : R) :
a * a - b * b = (a + b) * (a - b)

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

source
theorem mul_self_sub_one {R : Type x} [non_assoc_ring R] (a : R) :
a * a - 1 = (a + 1) * (a - 1)
source
theorem mul_self_eq_mul_self_iff {R : Type x} [comm_ring R] [no_zero_divisors R] {a b : R} :
a * a = b * b ↔ a = b ∨ a = -b
source
theorem mul_self_eq_one_iff {R : Type x} [non_assoc_ring R] [no_zero_divisors R] {a : R} :
a * a = 1 ↔ a = 1 ∨ a = -1
source
theorem units.inv_eq_self_iff {R : Type x} [ring R] [no_zero_divisors R] (u : Rˣ) :
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.