# mathlib3documentation

algebra.field.basic

# Lemmas about division (semi)rings and (semi)fields #

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

theorem add_div {α : Type u_1} (a b c : α) :
(a + b) / c = a / c + b / c
theorem div_add_div_same {α : Type u_1} (a b c : α) :
a / c + b / c = (a + b) / c
theorem same_add_div {α : Type u_1} {a b : α} (h : b 0) :
(b + a) / b = 1 + a / b
theorem div_add_same {α : Type u_1} {a b : α} (h : b 0) :
(a + b) / b = a / b + 1
theorem one_add_div {α : Type u_1} {a b : α} (h : b 0) :
1 + a / b = (b + a) / b
theorem div_add_one {α : Type u_1} {a b : α} (h : b 0) :
a / b + 1 = (a + b) / b
theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {α : Type u_1} {a b : α} (ha : a 0) (hb : b 0) :
1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
theorem add_div_eq_mul_add_div {α : Type u_1} {c : α} (a b : α) (hc : c 0) :
a + b / c = (a * c + b) / c
theorem add_div' {α : Type u_1} (a b c : α) (hc : c 0) :
b + a / c = (b * c + a) / c
theorem div_add' {α : Type u_1} (a b c : α) (hc : c 0) :
a / c + b = (a + b * c) / c
@[protected]
theorem commute.div_add_div {α : Type u_1} {a b c d : α} (hbc : c) (hbd : d) (hb : b 0) (hd : d 0) :
a / b + c / d = (a * d + b * c) / (b * d)
@[protected]
theorem commute.one_div_add_one_div {α : Type u_1} {a b : α} (hab : b) (ha : a 0) (hb : b 0) :
1 / a + 1 / b = (a + b) / (a * b)
@[protected]
theorem commute.inv_add_inv {α : Type u_1} {a b : α} (hab : b) (ha : a 0) (hb : b 0) :
a⁻¹ + b⁻¹ = (a + b) / (a * b)
theorem one_div_neg_one_eq_neg_one {K : Type u_3}  :
1 / -1 = -1
theorem one_div_neg_eq_neg_one_div {K : Type u_3} (a : K) :
1 / -a = -(1 / a)
theorem div_neg_eq_neg_div {K : Type u_3} (a b : K) :
b / -a = -(b / a)
theorem neg_div {K : Type u_3} (a b : K) :
-b / a = -(b / a)
theorem neg_div' {K : Type u_3} (a b : K) :
-(b / a) = -b / a
theorem neg_div_neg_eq {K : Type u_3} (a b : K) :
-a / -b = a / b
theorem neg_inv {K : Type u_3} {a : K} :
theorem div_neg {K : Type u_3} {b : K} (a : K) :
a / -b = -(a / b)
theorem inv_neg {K : Type u_3} {a : K} :
@[simp]
theorem div_neg_self {K : Type u_3} {a : K} (h : a 0) :
a / -a = -1
@[simp]
theorem neg_div_self {K : Type u_3} {a : K} (h : a 0) :
-a / a = -1
theorem div_sub_div_same {K : Type u_3} (a b c : K) :
a / c - b / c = (a - b) / c
theorem same_sub_div {K : Type u_3} {a b : K} (h : b 0) :
(b - a) / b = 1 - a / b
theorem one_sub_div {K : Type u_3} {a b : K} (h : b 0) :
1 - a / b = (b - a) / b
theorem div_sub_same {K : Type u_3} {a b : K} (h : b 0) :
(a - b) / b = a / b - 1
theorem div_sub_one {K : Type u_3} {a b : K} (h : b 0) :
a / b - 1 = (a - b) / b
theorem sub_div {K : Type u_3} (a b c : K) :
(a - b) / c = a / c - b / c
theorem inv_sub_inv' {K : Type u_3} {a b : K} (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹

See inv_sub_inv for the more convenient version when K is commutative.

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {K : Type u_3} {a b : K} (ha : a 0) (hb : b 0) :
1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
@[protected, instance]
def division_ring.is_domain {K : Type u_3}  :
@[protected]
theorem commute.div_sub_div {K : Type u_3} {a b c d : K} (hbc : c) (hbd : d) (hb : b 0) (hd : d 0) :
a / b - c / d = (a * d - b * c) / (b * d)
@[protected]
theorem commute.inv_sub_inv {K : Type u_3} {a b : K} (hab : b) (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = (b - a) / (a * b)
theorem div_add_div {α : Type u_1} [semifield α] {b d : α} (a c : α) (hb : b 0) (hd : d 0) :
a / b + c / d = (a * d + b * c) / (b * d)
theorem one_div_add_one_div {α : Type u_1} [semifield α] {a b : α} (ha : a 0) (hb : b 0) :
1 / a + 1 / b = (a + b) / (a * b)
theorem inv_add_inv {α : Type u_1} [semifield α] {a b : α} (ha : a 0) (hb : b 0) :
a⁻¹ + b⁻¹ = (a + b) / (a * b)
theorem div_sub_div {K : Type u_3} [field K] (a : K) {b : K} (c : K) {d : K} (hb : b 0) (hd : d 0) :
a / b - c / d = (a * d - b * c) / (b * d)
theorem inv_sub_inv {K : Type u_3} [field K] {a b : K} (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = (b - a) / (a * b)
theorem sub_div' {K : Type u_3} [field K] (a b c : K) (hc : c 0) :
b - a / c = (b * c - a) / c
theorem div_sub' {K : Type u_3} [field K] (a b c : K) (hc : c 0) :
a / c - b = (a - c * b) / c
@[protected, instance]
def field.is_domain {K : Type u_3} [field K] :
@[protected]
theorem ring_hom.injective {α : Type u_1} {β : Type u_2} [semiring β] [nontrivial β] (f : α →+* β) :
noncomputable def division_ring_of_is_unit_or_eq_zero {R : Type u_4} [nontrivial R] [hR : ring R] (h : (a : R), a = 0) :

Constructs a division_ring structure on a ring consisting only of units and 0.

Equations
@[reducible]
noncomputable def field_of_is_unit_or_eq_zero {R : Type u_4} [nontrivial R] [hR : comm_ring R] (h : (a : R), a = 0) :

Constructs a field structure on a comm_ring consisting only of units and 0. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.division_semiring {α : Type u_1} {β : Type u_2} [has_zero α] [has_mul α] [has_add α] [has_one α] [has_inv α] [has_div α] [ α] [ ] [ ] [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) (inv : (x : α), f x⁻¹ = (f x)⁻¹) (div : (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) (zpow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a division_semiring along an injective function.

Equations
@[protected, reducible]
def function.injective.division_ring {K : Type u_3} {K' : Type u_1} [has_zero K'] [has_one K'] [has_add K'] [has_mul K'] [has_neg K'] [has_sub K'] [has_inv K'] [has_div K'] [ K'] [ K'] [ K'] [has_pow K' ] [has_pow K' ] [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K'] (f : K' K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : K'), f (x + y) = f x + f y) (mul : (x y : K'), f (x * y) = f x * f y) (neg : (x : K'), f (-x) = -f x) (sub : (x y : K'), f (x - y) = f x - f y) (inv : (x : K'), f x⁻¹ = (f x)⁻¹) (div : (x y : K'), f (x / y) = f x / f y) (nsmul : (x : K') (n : ), f (n x) = n f x) (zsmul : (x : K') (n : ), f (n x) = n f x) (qsmul : (x : K') (n : ), f (n x) = n f x) (npow : (x : K') (n : ), f (x ^ n) = f x ^ n) (zpow : (x : K') (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) (rat_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.injective.semifield {α : Type u_1} {β : Type u_2} [semifield β] [has_zero α] [has_mul α] [has_add α] [has_one α] [has_inv α] [has_div α] [ α] [ ] [ ] [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) (inv : (x : α), f x⁻¹ = (f x)⁻¹) (div : (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) (zpow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a field along an injective function.

Equations
@[protected, reducible]
def function.injective.field {K : Type u_3} [field K] {K' : Type u_1} [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K'] [has_div K'] [ K'] [ K'] [ K'] [has_pow K' ] [has_pow K' ] [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K'] (f : K' K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : K'), f (x + y) = f x + f y) (mul : (x y : K'), f (x * y) = f x * f y) (neg : (x : K'), f (-x) = -f x) (sub : (x y : K'), f (x - y) = f x - f y) (inv : (x : K'), f x⁻¹ = (f x)⁻¹) (div : (x y : K'), f (x / y) = f x / f y) (nsmul : (x : K') (n : ), f (n x) = n f x) (zsmul : (x : K') (n : ), f (n x) = n f x) (qsmul : (x : K') (n : ), f (n x) = n f x) (npow : (x : K') (n : ), f (x ^ n) = f x ^ n) (zpow : (x : K') (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) (rat_cast : (n : ), f n = n) :

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

Equations

### Order dual #

@[protected, instance]
def order_dual.has_rat_cast {α : Type u_1} [h : has_rat_cast α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.division_ring {α : Type u_1} [h : division_ring α] :
Equations
@[protected, instance]
def order_dual.semifield {α : Type u_1} [h : semifield α] :
Equations
@[protected, instance]
def order_dual.field {α : Type u_1} [h : field α] :
Equations
@[simp]
theorem to_dual_rat_cast {α : Type u_1} [has_rat_cast α] (n : ) :
@[simp]
theorem of_dual_rat_cast {α : Type u_1} [has_rat_cast α] (n : ) :

### Lexicographic order #

@[protected, instance]
def lex.has_rat_cast {α : Type u_1} [h : has_rat_cast α] :
Equations
@[protected, instance]
def lex.division_semiring {α : Type u_1} [h : division_semiring α] :
Equations
@[protected, instance]
def lex.division_ring {α : Type u_1} [h : division_ring α] :
Equations
@[protected, instance]
def lex.semifield {α : Type u_1} [h : semifield α] :
Equations
@[protected, instance]
def lex.field {α : Type u_1} [h : field α] :
field (lex α)
Equations
@[simp]
theorem to_lex_rat_cast {α : Type u_1} [has_rat_cast α] (n : ) :
= n
@[simp]
theorem of_lex_rat_cast {α : Type u_1} [has_rat_cast α] (n : ) :