mathlib documentation

algebra.ring.basic

Semirings and rings #

This file defines semirings, rings and domains. This is analogous to algebra.group.defs and algebra.group.basic, the difference being that the former is about + and * separately, while the present file is about their interaction.

Main definitions #

Tags #

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 of this typeclass
Instances of other typeclasses for distrib
  • distrib.has_sizeof_inst
source
@[instance]
def distrib.to_has_add (R : Type u_1) [self : distrib R] :
has_add R
source
@[class]
structure left_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
Type
  • left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c

A typeclass stating that multiplication is left distributive over addition.

Instances of this typeclass
Instances of other typeclasses for left_distrib_class
  • left_distrib_class.has_sizeof_inst
source
@[class]
structure right_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
Type
  • right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c

A typeclass stating that multiplication is right distributive over addition.

Instances of this typeclass
Instances of other typeclasses for right_distrib_class
  • right_distrib_class.has_sizeof_inst
source
@[protected, instance]
def distrib.left_distrib_class (R : Type u_1) [distrib R] :
left_distrib_class R
Equations
source
@[protected, instance]
def distrib.right_distrib_class (R : Type u_1) [distrib R] :
right_distrib_class R
Equations
source
theorem left_distrib {R : Type x} [has_mul R] [has_add R] [left_distrib_class R] (a b c : R) :
a * (b + c) = a * b + a * c
source
theorem mul_add {R : Type x} [has_mul R] [has_add R] [left_distrib_class R] (a b c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

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

Alias of right_distrib.

source
theorem distrib_three_right {R : Type x} [has_mul R] [has_add R] [right_distrib_class 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 of this typeclass
Instances of other typeclasses for non_unital_non_assoc_semiring
  • non_unital_non_assoc_semiring.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for non_unital_semiring
  • non_unital_semiring.has_sizeof_inst
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
@[instance]
def non_assoc_semiring.to_add_comm_monoid_with_one (α : Type u) [self : non_assoc_semiring α] :
add_comm_monoid_with_one α
source
@[class]
structure non_assoc_semiring (α : Type u) :
Type u

A unital but not-necessarily-associative semiring.

Instances of this typeclass
Instances of other typeclasses for non_assoc_semiring
  • non_assoc_semiring.has_sizeof_inst
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
  • nat_cast : ℕ → α
  • nat_cast_zero : semiring.nat_cast 0 = 0 . "control_laws_tac"
  • nat_cast_succ : (∀ (n : ℕ), semiring.nat_cast (n + 1) = semiring.nat_cast n + 1) . "control_laws_tac"
  • 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 of this typeclass
Instances of other typeclasses for semiring
  • semiring.has_sizeof_inst
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 u} [non_assoc_semiring α] {β : Type v} [has_zero β] [has_one β] [has_mul β] [has_add β] [has_scalar ℕ β] [has_nat_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :
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 u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_scalar ℕ β] [has_nat_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑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 u} [non_assoc_semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_scalar ℕ β] [has_nat_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :
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 u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_scalar ℕ β] [has_nat_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :
semiring β

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

Equations
source
theorem one_add_one_eq_two {α : Type u} [has_one α] [has_add α] :
1 + 1 = 2
source
theorem dvd_add {α : Type u} [has_add α] [semigroup α] [left_distrib_class α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b + c
source
theorem add_one_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(a + 1) * b = a * b + b
source
theorem mul_add_one {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (b + 1) = a * b + a
source
theorem one_add_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(1 + a) * b = b + a * b
source
theorem mul_one_add {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (1 + b) = a + a * b
source
theorem two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
2 * n = n + n
source
theorem bit0_eq_two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
bit0 n = 2 * n
source
theorem mul_two {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (n : α) :
n * 2 = n + 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
@[simp]
theorem map_bit0 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [add_hom_class F α β] (f : F) (a : α) :
⇑f (bit0 a) = bit0 (⇑f a)

Additive homomorphisms preserve bit0.

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

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

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

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

Equations
source
@[simp]
theorem add_monoid_hom.coe_mul_right {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
⇑(add_monoid_hom.mul_right r) = λ (_x : R), _x * r
source
theorem add_monoid_hom.mul_right_apply {R : Type u_1} [non_unital_non_assoc_semiring R] (a r : R) :
⇑(add_monoid_hom.mul_right r) a = a * r
source
@[simp]
theorem two_dvd_bit0 {α : Type u} [semiring α] {a : α} :
2 ∣ bit0 a
source
@[class]
structure non_unital_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 : α), non_unital_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_comm_semiring.nsmul n.succ x = x + non_unital_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)
  • mul_comm : ∀ (a b : α), a * b = b * a

A non-unital commutative semiring is a non_unital_semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), commutative semigroup (comm_semigroup), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances of this typeclass
Instances of other typeclasses for non_unital_comm_semiring
  • non_unital_comm_semiring.has_sizeof_inst
source
@[instance]
def non_unital_comm_semiring.to_comm_semigroup (α : Type u) [self : non_unital_comm_semiring α] :
comm_semigroup α
source
@[instance]
def non_unital_comm_semiring.to_non_unital_semiring (α : Type u) [self : non_unital_comm_semiring α] :
non_unital_semiring α
source
@[protected]
def function.injective.non_unital_comm_semiring {α : Type u} {γ : Type w} [non_unital_comm_semiring α] [has_zero γ] [has_add γ] [has_mul γ] [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) (nsmul : ∀ (x : γ) (n : ℕ), f (n • x) = n • f x) :
non_unital_comm_semiring γ

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

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

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

Equations
source
theorem has_dvd.dvd.linear_comb {α : Type u} [non_unital_comm_semiring α] {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) :
d ∣ a * x + b * y
source
@[class]
structure comm_semiring (α : Type u) :
Type u

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 of this typeclass
Instances of other typeclasses for comm_semiring
  • comm_semiring.has_sizeof_inst
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 α
Instances for comm_semiring.to_semiring
source
@[protected, instance]
def comm_semiring.to_non_unital_comm_semiring {α : Type u} [comm_semiring α] :
non_unital_comm_semiring α
Equations
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_nat_cast γ] [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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑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_nat_cast γ] [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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑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
@[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 of this typeclass
Instances of other typeclasses for has_distrib_neg
  • has_distrib_neg.has_sizeof_inst
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
@[protected]
def function.injective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_distrib_neg α] [has_neg β] [has_mul β] (f : β → α) (hf : function.injective f) (neg : ∀ (a : β), f (-a) = -f a) (mul : ∀ (a b : β), f (a * b) = f a * f b) :
has_distrib_neg β

A type endowed with - and * has distributive negation, if it admits an injective map that preserves - and * to a type which has distributive negation.

Equations
source
@[protected]
def function.surjective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_distrib_neg α] [has_neg β] [has_mul β] (f : α → β) (hf : function.surjective f) (neg : ∀ (a : α), f (-a) = -f a) (mul : ∀ (a b : α), f (a * b) = f a * f b) :
has_distrib_neg β

A type endowed with - and * has distributive negation, if it admits a surjective map that preserves - and * from a type which has distributive negation.

Equations
source
@[protected, instance]
def add_opposite.has_distrib_neg {α : Type u} [has_mul α] [has_distrib_neg α] :
has_distrib_neg αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.has_distrib_neg {α : Type u} [has_mul α] [has_distrib_neg α] :
has_distrib_neg αᵐᵒᵖ
Equations
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 subtraction_monoid is available.

source
theorem dvd_neg_of_dvd {α : Type u} [semigroup α] [has_distrib_neg α] {a b : α} (h : a ∣ b) :
a ∣ -b
source
theorem dvd_of_dvd_neg {α : Type u} [semigroup α] [has_distrib_neg α] {a b : α} (h : a ∣ -b) :
a ∣ b
source
@[simp]
theorem dvd_neg {α : Type u} [semigroup α] [has_distrib_neg α] (a b : α) :
a ∣ -b ↔ a ∣ b

An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

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

The negation of an element a of a semigroup with a distributive negation divides another element b iff a divides b.

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 of this typeclass
Instances of other typeclasses for non_unital_non_assoc_ring
  • non_unital_non_assoc_ring.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for non_unital_ring
  • non_unital_ring.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for non_assoc_ring
  • non_assoc_ring.has_sizeof_inst
source
@[instance]
def non_assoc_ring.to_add_group_with_one (α : Type u_1) [self : non_assoc_ring α] :
add_group_with_one α
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 ℤ β] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) :
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 ℤ β] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) :
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_monoid (α : Type u) [self : ring α] :
monoid α
source
@[instance]
def ring.to_add_comm_group_with_one (α : Type u) [self : ring α] :
add_comm_group_with_one α
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
  • int_cast : ℤ → α
  • nat_cast : ℕ → α
  • one : α
  • nat_cast_zero : ring.nat_cast 0 = 0 . "control_laws_tac"
  • nat_cast_succ : (∀ (n : ℕ), ring.nat_cast (n + 1) = ring.nat_cast n + 1) . "control_laws_tac"
  • int_cast_of_nat : (∀ (n : ℕ), ring.int_cast ↑n = ↑n) . "control_laws_tac"
  • int_cast_neg_succ_of_nat : (∀ (n : ℕ), ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
  • mul : α → α → α
  • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
  • 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 of this typeclass
Instances of other typeclasses for ring
  • ring.has_sizeof_inst
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
Instances for ring.to_semiring
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 β ℕ] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑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 β ℕ] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑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
@[class]
structure non_unital_comm_ring (α : Type u) :
Type u

A non-unital commutative ring is a non_unital_ring with commutative multiplication.

Instances of this typeclass
Instances of other typeclasses for non_unital_comm_ring
  • non_unital_comm_ring.has_sizeof_inst
source
@[instance]
def non_unital_comm_ring.to_comm_semigroup (α : Type u) [self : non_unital_comm_ring α] :
comm_semigroup α
source
@[instance]
def non_unital_comm_ring.to_non_unital_ring (α : Type u) [self : non_unital_comm_ring α] :
non_unital_ring α
source
@[protected, instance]
def non_unital_comm_ring.to_non_unital_comm_semiring {α : Type u} [s : non_unital_comm_ring α] :
non_unital_comm_semiring α
Equations
source
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
Instances for comm_ring.to_ring
source
@[class]
structure comm_ring (α : Type u) :
Type u

A commutative ring is a ring with commutative multiplication.

Instances of this typeclass
Instances of other typeclasses for comm_ring
  • comm_ring.has_sizeof_inst
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
@[protected, instance]
def comm_ring.to_non_unital_comm_ring {α : Type u} [s : comm_ring α] :
non_unital_comm_ring α
Equations
source
theorem dvd_sub {α : Type u} [non_unital_ring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b - c
source
theorem dvd_add_iff_left {α : Type u} [non_unital_ring α] {a b c : α} (h : a ∣ c) :
a ∣ b ↔ a ∣ b + c
source
theorem dvd_add_iff_right {α : Type u} [non_unital_ring α] {a b c : α} (h : a ∣ b) :
a ∣ c ↔ a ∣ b + c
source
theorem dvd_add_left {α : Type u} [non_unital_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} [non_unital_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
theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [non_unital_ring α] {a b c : α} (h : a ∣ b - c) :
a ∣ b ↔ a ∣ c
source
theorem two_dvd_bit1 {α : Type u} [ring α] {a : α} :
2 ∣ bit1 a ↔ 2 ∣ 1
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
@[protected]
def function.injective.non_unital_comm_ring {α : Type u} {β : Type v} [non_unital_comm_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_comm_ring β

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

Equations
source
@[protected]
def function.surjective.non_unital_comm_ring {α : Type u} {β : Type v} [non_unital_comm_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_comm_ring β

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

Equations
source
theorem Vieta_formula_quadratic {α : Type u} [non_unital_comm_ring α] {b c x : α} (h : x * x - b * x + c = 0) :
∃ (y : α), y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with its roots. This particular version states that if we have a root x of a monic quadratic polynomial, then there is another root y such that x + y is negative the a_1 coefficient and x * y is the a_0 coefficient.

source
theorem dvd_mul_sub_mul {α : Type u} [non_unital_comm_ring α] {k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) :
k ∣ a * x - b * y
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 β ℕ] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑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 β ℕ] [has_nat_cast β] [has_int_cast β] (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) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) :
comm_ring β

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

Equations
source
theorem succ_ne_self {α : Type u} [non_assoc_ring α] [nontrivial α] (a : α) :
a + 1 ≠ a
source
theorem pred_ne_self {α : Type u} [non_assoc_ring α] [nontrivial α] (a : α) :
a - 1 ≠ a
source
theorem is_left_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} [non_unital_non_assoc_ring α] [no_zero_divisors α] {k : α} (hk : k ≠ 0) :
is_regular k
source
theorem is_regular_iff_ne_zero' {α : Type u} [nontrivial α] [non_unital_non_assoc_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
def no_zero_divisors.to_cancel_comm_monoid_with_zero {α : Type u} [comm_ring α] [no_zero_divisors α] :
cancel_comm_monoid_with_zero α

A commutative ring with no zero divisors is a cancel_comm_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 of this typeclass
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, instance]
def is_domain.to_cancel_comm_monoid_with_zero {α : Type u} [comm_ring α] [is_domain α] :
cancel_comm_monoid_with_zero α
Equations
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} [non_unital_non_assoc_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} [non_unital_non_assoc_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]