doc-next-gen

Mathlib.Algebra.Field.Basic

Module docstring

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

","### Order dual ","### Lexicographic order "}

add_div theorem
(a b c : K) : (a + b) / c = a / c + b / c
Full source 
theorem add_div (a b c : K) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
Right Distributivity of Division over Addition: $(a + b)/c = a/c + b/c$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$, the division operation distributes over addition as $(a + b) / c = a / c + b / c$.
div_add_div_same theorem
(a b c : K) : a / c + b / c = (a + b) / c
Full source 
@[field_simps]
theorem div_add_div_same (a b c : K) : a / c + b / c = (a + b) / c :=
  (add_div _ _ _).symm
Sum of Fractions with Common Denominator: $a/c + b/c = (a + b)/c$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$, the sum of $a/c$ and $b/c$ equals $(a + b)/c$.
same_add_div theorem
(h : b ≠ 0) : (b + a) / b = 1 + a / b
Full source 
theorem same_add_div (h : b ≠ 0) : (b + a) / b = 1 + a / b := by rw [← div_self h, add_div]
Simplification of $(b + a)/b$ to $1 + a/b$ for nonzero $b$
Informal description
For any nonzero element $b$ in a division ring $K$ and any element $a$ in $K$, the expression $(b + a)/b$ simplifies to $1 + a/b$.
div_add_same theorem
(h : b ≠ 0) : (a + b) / b = a / b + 1
Full source 
theorem div_add_same (h : b ≠ 0) : (a + b) / b = a / b + 1 := by rw [← div_self h, add_div]
Simplification of $(a + b)/b$ to $a/b + 1$ for nonzero $b$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, the expression $(a + b)/b$ simplifies to $a/b + 1$.
one_add_div theorem
(h : b ≠ 0) : 1 + a / b = (b + a) / b
Full source 
theorem one_add_div (h : b ≠ 0) : 1 + a / b = (b + a) / b :=
  (same_add_div h).symm
Identity: $1 + a/b = (b + a)/b$ for nonzero $b$
Informal description
For any nonzero element $b$ in a division ring $K$ and any element $a$ in $K$, the expression $1 + a/b$ is equal to $(b + a)/b$.
div_add_one theorem
(h : b ≠ 0) : a / b + 1 = (a + b) / b
Full source 
theorem div_add_one (h : b ≠ 0) : a / b + 1 = (a + b) / b :=
  (div_add_same h).symm
Simplification of $a/b + 1$ to $(a + b)/b$ for nonzero $b$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, the expression $a/b + 1$ simplifies to $(a + b)/b$.
inv_add_inv' theorem
(ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹
Full source 
/-- See `inv_add_inv` for the more convenient version when `K` is commutative. -/
theorem inv_add_inv' (ha : a ≠ 0) (hb : b ≠ 0) :
    a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹ :=
  let _ := invertibleOfNonzero ha; let _ := invertibleOfNonzero hb; invOf_add_invOf a b
Sum of Inverses Formula in Division Rings
Informal description
For any nonzero elements $a$ and $b$ in a division ring $K$, the sum of their inverses equals $a^{-1} \cdot (a + b) \cdot b^{-1}$, i.e., \[ a^{-1} + b^{-1} = a^{-1} \cdot (a + b) \cdot b^{-1}. \]
one_div_mul_add_mul_one_div_eq_one_div_add_one_div theorem
(ha : a ≠ 0) (hb : b ≠ 0) : 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
Full source 
theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (a + b) * (1 / b) = 1 / a + 1 / b := by
  simpa only [one_div] using (inv_add_inv' ha hb).symm
Reciprocal Product-Sum Identity: $\frac{1}{a}(a+b)\frac{1}{b} = \frac{1}{a} + \frac{1}{b}$
Informal description
For any nonzero elements $a$ and $b$ in a division ring $K$, the following identity holds: \[ \frac{1}{a} \cdot (a + b) \cdot \frac{1}{b} = \frac{1}{a} + \frac{1}{b}. \]
add_div_eq_mul_add_div theorem
(a b : K) (hc : c ≠ 0) : a + b / c = (a * c + b) / c
Full source 
theorem add_div_eq_mul_add_div (a b : K) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
  (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel₀ _ hc]
Addition-Division Identity: $a + \frac{b}{c} = \frac{a c + b}{c}$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$ with $c \neq 0$, the expression $a + \frac{b}{c}$ is equal to $\frac{a \cdot c + b}{c}$.
add_div' theorem
(a b c : K) (hc : c ≠ 0) : b + a / c = (b * c + a) / c
Full source 
@[field_simps]
theorem add_div' (a b c : K) (hc : c ≠ 0) : b + a / c = (b * c + a) / c := by
  rw [add_div, mul_div_cancel_right₀ _ hc]
Right Addition with Division: $b + \frac{a}{c} = \frac{b c + a}{c}$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$ with $c \neq 0$, we have $b + \frac{a}{c} = \frac{b \cdot c + a}{c}$.
div_add' theorem
(a b c : K) (hc : c ≠ 0) : a / c + b = (a + b * c) / c
Full source 
@[field_simps]
theorem div_add' (a b c : K) (hc : c ≠ 0) : a / c + b = (a + b * c) / c := by
  rwa [add_comm, add_div', add_comm]
Left Addition with Division: $\frac{a}{c} + b = \frac{a + b c}{c}$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$ with $c \neq 0$, we have $\frac{a}{c} + b = \frac{a + b \cdot c}{c}$.
Commute.div_add_div theorem
(hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d)
Full source 
protected theorem Commute.div_add_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0)
    (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d) := by
  rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
Addition of Fractions with Commuting Elements: $\frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}$
Informal description
Let $a, b, c, d$ be elements in a division ring such that $b$ commutes with $c$ and $d$, and $b, d \neq 0$. Then: \[ \frac{a}{b} + \frac{c}{d} = \frac{a \cdot d + b \cdot c}{b \cdot d} \]
Commute.one_div_add_one_div theorem
(hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b)
Full source 
protected theorem Commute.one_div_add_one_div (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a + 1 / b = (a + b) / (a * b) := by
  rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
Reciprocal Addition Formula for Commuting Elements: $\frac{1}{a} + \frac{1}{b} = \frac{a+b}{ab}$
Informal description
Let $a$ and $b$ be nonzero elements in a division ring such that $a$ commutes with $b$. Then the sum of their reciprocals equals the sum of the elements divided by their product: \[ \frac{1}{a} + \frac{1}{b} = \frac{a + b}{a \cdot b} \]
Commute.inv_add_inv theorem
(hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b)
Full source 
protected theorem Commute.inv_add_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    a⁻¹ + b⁻¹ = (a + b) / (a * b) := by
  rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
Inverse Addition Formula for Commuting Elements: $a^{-1} + b^{-1} = \frac{a+b}{ab}$
Informal description
Let $a$ and $b$ be nonzero elements in a division ring such that $a$ commutes with $b$. Then the sum of their inverses equals the sum of the elements divided by their product: \[ a^{-1} + b^{-1} = \frac{a + b}{a \cdot b} \]
add_self_div_two theorem
(a : K) : (a + a) / 2 = a
Full source 
@[simp] lemma add_self_div_two (a : K) : (a + a) / 2 = a := by
  rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]
Average Identity: $\frac{a + a}{2} = a$ in Division Semirings
Informal description
For any element $a$ in a division semiring $K$, the sum of $a$ with itself divided by $2$ equals $a$, i.e., $\frac{a + a}{2} = a$.
add_halves theorem
(a : K) : a / 2 + a / 2 = a
Full source 
@[simp] lemma add_halves (a : K) : a / 2 + a / 2 = a := by rw [← add_div, add_self_div_two]
Halving Identity: $\frac{a}{2} + \frac{a}{2} = a$ in Division Semirings
Informal description
For any element $a$ in a division semiring $K$, the sum of $a/2$ with itself equals $a$, i.e., $\frac{a}{2} + \frac{a}{2} = a$.
div_neg_self theorem
{a : K} (h : a ≠ 0) : a / -a = -1
Full source 
@[simp]
theorem div_neg_self {a : K} (h : a ≠ 0) : a / -a = -1 := by rw [div_neg_eq_neg_div, div_self h]
Division by Negative Self: $a / (-a) = -1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a division ring $K$, the division of $a$ by its additive inverse $-a$ yields the additive inverse of the multiplicative identity, i.e., $a / (-a) = -1$.
neg_div_self theorem
{a : K} (h : a ≠ 0) : -a / a = -1
Full source 
@[simp]
theorem neg_div_self {a : K} (h : a ≠ 0) : -a / a = -1 := by rw [neg_div, div_self h]
Negative Division Identity: $-a / a = -1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a division ring $K$, the division of $-a$ by $a$ equals $-1$, i.e., $-a / a = -1$.
div_sub_div_same theorem
(a b c : K) : a / c - b / c = (a - b) / c
Full source 
theorem div_sub_div_same (a b c : K) : a / c - b / c = (a - b) / c := by
  rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg]
Difference of Fractions with Common Denominator: $a/c - b/c = (a - b)/c$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$, the difference of $a/c$ and $b/c$ equals $(a - b)/c$.
same_sub_div theorem
{a b : K} (h : b ≠ 0) : (b - a) / b = 1 - a / b
Full source 
theorem same_sub_div {a b : K} (h : b ≠ 0) : (b - a) / b = 1 - a / b := by
  simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm
Fractional Identity: $\frac{b - a}{b} = 1 - \frac{a}{b}$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, we have $\frac{b - a}{b} = 1 - \frac{a}{b}$.
one_sub_div theorem
{a b : K} (h : b ≠ 0) : 1 - a / b = (b - a) / b
Full source 
theorem one_sub_div {a b : K} (h : b ≠ 0) : 1 - a / b = (b - a) / b :=
  (same_sub_div h).symm
Fractional Identity: $1 - \frac{a}{b} = \frac{b - a}{b}$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, we have $1 - \frac{a}{b} = \frac{b - a}{b}$.
div_sub_same theorem
{a b : K} (h : b ≠ 0) : (a - b) / b = a / b - 1
Full source 
theorem div_sub_same {a b : K} (h : b ≠ 0) : (a - b) / b = a / b - 1 := by
  simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm
Quotient Identity: $(a - b)/b = a/b - 1$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, the quotient $(a - b)/b$ equals $a/b - 1$.
div_sub_one theorem
{a b : K} (h : b ≠ 0) : a / b - 1 = (a - b) / b
Full source 
theorem div_sub_one {a b : K} (h : b ≠ 0) : a / b - 1 = (a - b) / b :=
  (div_sub_same h).symm
Quotient-to-Difference Identity: $a/b - 1 = (a - b)/b$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a division ring $K$ with $b \neq 0$, the difference $a/b - 1$ equals $(a - b)/b$.
sub_div theorem
(a b c : K) : (a - b) / c = a / c - b / c
Full source 
theorem sub_div (a b c : K) : (a - b) / c = a / c - b / c :=
  (div_sub_div_same _ _ _).symm
Difference-to-Quotient Identity: $(a - b)/c = a/c - b/c$
Informal description
For any elements $a$, $b$, and $c$ in a division ring $K$, the quotient of the difference $(a - b)$ by $c$ equals the difference of the quotients $a/c$ and $b/c$, i.e., $(a - b)/c = a/c - b/c$.
inv_sub_inv' theorem
{a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
Full source 
/-- See `inv_sub_inv` for the more convenient version when `K` is commutative. -/
theorem inv_sub_inv' {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹ :=
  let _ := invertibleOfNonzero ha; let _ := invertibleOfNonzero hb; invOf_sub_invOf a b
Difference of Inverses Formula in Division Rings
Informal description
For any nonzero elements $a$ and $b$ in a division ring $K$, the difference of their inverses satisfies $a^{-1} - b^{-1} = a^{-1} \cdot (b - a) \cdot b^{-1}$.
one_div_mul_sub_mul_one_div_eq_one_div_add_one_div theorem
(ha : a ≠ 0) (hb : b ≠ 0) : 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
Full source 
theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (b - a) * (1 / b) = 1 / a - 1 / b := by
  simpa only [one_div] using (inv_sub_inv' ha hb).symm
Reciprocal Difference Identity: $\frac{1}{a}(b-a)\frac{1}{b} = \frac{1}{a}-\frac{1}{b}$
Informal description
For any nonzero elements $a$ and $b$ in a division ring $K$, the following identity holds: $$ \frac{1}{a} \cdot (b - a) \cdot \frac{1}{b} = \frac{1}{a} - \frac{1}{b} $$
Commute.div_sub_div theorem
(hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)
Full source 
protected theorem Commute.div_sub_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0)
    (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d) := by
  simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd
Subtraction of Fractions with Commuting Elements: $\frac{a}{b} - \frac{c}{d} = \frac{ad - bc}{bd}$
Informal description
Let $a, b, c, d$ be elements in a division ring such that $b$ commutes with $c$ and $d$, and $b, d \neq 0$. Then: \[ \frac{a}{b} - \frac{c}{d} = \frac{a \cdot d - b \cdot c}{b \cdot d} \]
Commute.inv_sub_inv theorem
(hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b)
Full source 
protected theorem Commute.inv_sub_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    a⁻¹ - b⁻¹ = (b - a) / (a * b) := by
  simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]
Difference of Inverses Formula for Commuting Elements: $a^{-1} - b^{-1} = \frac{b - a}{ab}$
Informal description
Let $a$ and $b$ be commuting elements in a division ring such that $a, b \neq 0$. Then the difference of their inverses satisfies: \[ a^{-1} - b^{-1} = \frac{b - a}{a \cdot b} \]
sub_half theorem
(a : K) : a - a / 2 = a / 2
Full source 
lemma sub_half (a : K) : a - a / 2 = a / 2 := by rw [sub_eq_iff_eq_add, add_halves]
Subtraction of Half Identity: $a - \frac{a}{2} = \frac{a}{2}$ in Division Semirings
Informal description
For any element $a$ in a division semiring $K$, the difference between $a$ and its half equals its half, i.e., $a - \frac{a}{2} = \frac{a}{2}$.
half_sub theorem
(a : K) : a / 2 - a = -(a / 2)
Full source 
lemma half_sub (a : K) : a / 2 - a = -(a / 2) := by rw [← neg_sub, sub_half]
Half Subtraction Identity: $\frac{a}{2} - a = -\frac{a}{2}$
Informal description
For any element $a$ in a division semiring $K$, the difference between half of $a$ and $a$ equals the negation of half of $a$, i.e., $\frac{a}{2} - a = -\frac{a}{2}$.
div_add_div theorem
(a : K) (c : K) (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d)
Full source 
theorem div_add_div (a : K) (c : K) (hb : b ≠ 0) (hd : d ≠ 0) :
    a / b + c / d = (a * d + b * c) / (b * d) :=
  (Commute.all b _).div_add_div (Commute.all _ _) hb hd
Fraction Addition Formula: $\frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}$
Informal description
For any elements $a, c$ in a division semiring $K$ and nonzero elements $b, d \in K$, we have: \[ \frac{a}{b} + \frac{c}{d} = \frac{a \cdot d + b \cdot c}{b \cdot d} \]
one_div_add_one_div theorem
(ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b)
Full source 
theorem one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
  (Commute.all a _).one_div_add_one_div ha hb
Reciprocal Addition Formula: $\frac{1}{a} + \frac{1}{b} = \frac{a+b}{ab}$
Informal description
For any nonzero elements $a$ and $b$ in a division semiring, the sum of their reciprocals equals the sum of the elements divided by their product: \[ \frac{1}{a} + \frac{1}{b} = \frac{a + b}{a \cdot b} \]
inv_add_inv theorem
(ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b)
Full source 
theorem inv_add_inv (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b) :=
  (Commute.all a _).inv_add_inv ha hb
Inverse Addition Formula: $a^{-1} + b^{-1} = \frac{a+b}{ab}$
Informal description
For any nonzero elements $a$ and $b$ in a division ring, the sum of their inverses equals the sum of the elements divided by their product: \[ a^{-1} + b^{-1} = \frac{a + b}{a \cdot b} \]
div_sub_div theorem
(a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)
Full source 
@[field_simps]
theorem div_sub_div (a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) :
    a / b - c / d = (a * d - b * c) / (b * d) :=
  (Commute.all b _).div_sub_div (Commute.all _ _) hb hd
Subtraction of Fractions Formula: $\frac{a}{b} - \frac{c}{d} = \frac{ad - bc}{bd}$
Informal description
For any elements $a, c$ and nonzero elements $b, d$ in a division ring $K$, we have: \[ \frac{a}{b} - \frac{c}{d} = \frac{a \cdot d - b \cdot c}{b \cdot d} \]
inv_sub_inv theorem
{a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b)
Full source 
theorem inv_sub_inv {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) := by
  rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]
Difference of Inverses Formula: $a^{-1} - b^{-1} = \frac{b-a}{ab}$
Informal description
For any nonzero elements $a$ and $b$ in a division ring $K$, the difference of their inverses equals the difference of the elements divided by their product: \[ a^{-1} - b^{-1} = \frac{b - a}{a \cdot b} \]
sub_div' theorem
{a b c : K} (hc : c ≠ 0) : b - a / c = (b * c - a) / c
Full source 
@[field_simps]
theorem sub_div' {a b c : K} (hc : c ≠ 0) : b - a / c = (b * c - a) / c := by
  simpa using div_sub_div b a one_ne_zero hc
Subtraction of Fraction Formula: $b - \frac{a}{c} = \frac{bc - a}{c}$
Informal description
For any elements $a, b$ and nonzero element $c$ in a division ring $K$, we have: \[ b - \frac{a}{c} = \frac{b \cdot c - a}{c} \]
div_sub' theorem
{a b c : K} (hc : c ≠ 0) : a / c - b = (a - c * b) / c
Full source 
@[field_simps]
theorem div_sub' {a b c : K} (hc : c ≠ 0) : a / c - b = (a - c * b) / c := by
  simpa using div_sub_div a b hc one_ne_zero
Fraction Subtraction Formula: $\frac{a}{c} - b = \frac{a - c b}{c}$
Informal description
For any elements $a, b$ and nonzero element $c$ in a division ring $K$, we have: \[ \frac{a}{c} - b = \frac{a - c \cdot b}{c} \]
DivisionRing.ofIsUnitOrEqZero abbrev
[Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) : DivisionRing R
Full source 
/-- Constructs a `DivisionRing` structure on a `Ring` consisting only of units and 0. -/
-- See note [reducible non-instances]
noncomputable abbrev DivisionRing.ofIsUnitOrEqZero [Ring R] (h : ∀ a : R, IsUnitIsUnit a ∨ a = 0) :
    DivisionRing R where
  toRing := ‹Ring R›
  __ := groupWithZeroOfIsUnitOrEqZero h
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl
Division Ring Structure on a Ring with All Nonzero Elements Units
Informal description
Given a ring $R$ where every element is either a unit or zero, there exists a division ring structure on $R$.
Field.ofIsUnitOrEqZero abbrev
[CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) : Field R
Full source 
/-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0. -/
-- See note [reducible non-instances]
noncomputable abbrev Field.ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnitIsUnit a ∨ a = 0) :
    Field R where
  toCommRing := ‹CommRing R›
  __ := DivisionRing.ofIsUnitOrEqZero h
Field Structure on Commutative Ring with All Nonzero Elements Units
Informal description
Given a commutative ring $R$ where every element is either a unit or zero, there exists a field structure on $R$.
Function.Injective.divisionSemiring abbrev
[DivisionSemiring L] (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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring K
Full source 
/-- Pullback a `DivisionSemiring` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev divisionSemiring [DivisionSemiring L] (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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring K where
  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
  __ := hf.groupWithZero f zero one mul inv div npow zpow
  nnratCast_def q := hf <| by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
  nnqsmul := (· • ·)
  nnqsmul_def q a := hf <| by rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
Lifting Division Semiring Structure Along an Injective Homomorphism
Informal description
Let $L$ be a division semiring and $K$ a type equipped with zero, one, addition, multiplication, inversion, division, natural scalar multiplication, nonnegative rational scalar multiplication, natural and integer power operations, and natural number and nonnegative rational number embeddings. Given an injective function $f \colon K \to L$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x + y) = f(x) + f(y)$ for all $x, y \in K$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in K$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in K$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}_{\geq 0}$ and $x \in K$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{Z}$, - $f(n) = n$ for all $n \in \mathbb{N}$, - $f(q) = q$ for all $q \in \mathbb{Q}_{\geq 0}$, then $K$ inherits a division semiring structure from $L$ via $f$.
Function.Injective.divisionRing abbrev
[DivisionRing L] (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) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) (ratCast : ∀ q : ℚ, f q = q) : DivisionRing K
Full source 
/-- Pullback a `DivisionSemiring` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev divisionRing [DivisionRing L] (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) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
    (div : ∀ x y, f (x / y) = f x / f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
    (ratCast : ∀ q : ℚ, f q = q) : DivisionRing K where
  toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
  __ := hf.groupWithZero f zero one mul inv div npow zpow
  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
  ratCast_def q := hf <| by rw [ratCast, div, intCast, natCast, Rat.cast_def]
  qsmul := (· • ·)
  qsmul_def q a := hf <| by rw [qsmul, mul, Rat.smul_def, ratCast]
Lifting Division Ring Structure Along an Injective Homomorphism
Informal description
Let $L$ be a division ring and $K$ a type equipped with zero, one, addition, multiplication, negation, subtraction, inversion, division, natural and integer scalar multiplication, nonnegative rational and rational scalar multiplication, natural and integer power operations, and natural number, integer, nonnegative rational, and rational number embeddings. Given an injective function $f \colon K \to L$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x + y) = f(x) + f(y)$ for all $x, y \in K$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in K$, - $f(-x) = -f(x)$ for all $x \in K$, - $f(x - y) = f(x) - f(y)$ for all $x, y \in K$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in K$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}_{\geq 0}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}$ and $x \in K$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{Z}$, - $f(n) = n$ for all $n \in \mathbb{N}$, - $f(n) = n$ for all $n \in \mathbb{Z}$, - $f(q) = q$ for all $q \in \mathbb{Q}_{\geq 0}$, - $f(q) = q$ for all $q \in \mathbb{Q}$, then $K$ inherits a division ring structure from $L$ via $f$.
Function.Injective.semifield abbrev
[Semifield L] (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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield K
Full source 
/-- Pullback a `Field` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev semifield [Semifield L] (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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield K where
  toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
  __ := hf.commGroupWithZero f zero one mul inv div npow zpow
  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
Lifting Semifield Structure Along an Injective Homomorphism
Informal description
Let $L$ be a semifield and $K$ a type equipped with zero, one, addition, multiplication, inversion, division, natural scalar multiplication, nonnegative rational scalar multiplication, natural and integer power operations, and natural number and nonnegative rational number embeddings. Given an injective function $f \colon K \to L$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x + y) = f(x) + f(y)$ for all $x, y \in K$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in K$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in K$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}_{\geq 0}$ and $x \in K$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{Z}$, - $f(n) = n$ for all $n \in \mathbb{N}$, - $f(q) = q$ for all $q \in \mathbb{Q}_{\geq 0}$, then $K$ inherits a semifield structure from $L$ via $f$.
Function.Injective.field abbrev
[Field L] (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) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) (ratCast : ∀ q : ℚ, f q = q) : Field K
Full source 
/-- Pullback a `Field` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev field [Field L] (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) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
    (div : ∀ x y, f (x / y) = f x / f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
    (ratCast : ∀ q : ℚ, f q = q) :
    Field K where
  toCommRing := hf.commRing f zero one add mul neg sub nsmul zsmul npow natCast intCast
  __ := hf.divisionRing f zero one add mul neg sub inv div nsmul zsmul nnqsmul qsmul npow zpow
    natCast intCast nnratCast ratCast
Field Structure Lifting Along an Injective Homomorphism
Informal description
Let $L$ be a field and $f \colon K \to L$ an injective function satisfying: - $f(0) = 0$, - $f(1) = 1$, - $f(x + y) = f(x) + f(y)$ for all $x, y \in K$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in K$, - $f(-x) = -f(x)$ for all $x \in K$, - $f(x - y) = f(x) - f(y)$ for all $x, y \in K$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in K$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in K$, - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}_{\geq 0}$ and $x \in K$, - $f(q \cdot x) = q \cdot f(x)$ for all $q \in \mathbb{Q}$ and $x \in K$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in K$ and $n \in \mathbb{Z}$, - $f(n) = n$ for all $n \in \mathbb{N}$, - $f(n) = n$ for all $n \in \mathbb{Z}$, - $f(q) = q$ for all $q \in \mathbb{Q}_{\geq 0}$, - $f(q) = q$ for all $q \in \mathbb{Q}$. Then $K$ inherits a field structure from $L$ via $f$.
OrderDual.instRatCast instance
[RatCast K] : RatCast Kᵒᵈ
Full source 
instance instRatCast [RatCast K] : RatCast Kᵒᵈ := ‹_›
Rational Number Casting on Order Duals
Informal description
For any type $K$ with a rational number casting operation, the order dual $K^{\text{op}}$ also has a rational number casting operation.
OrderDual.instDivisionSemiring instance
[DivisionSemiring K] : DivisionSemiring Kᵒᵈ
Full source 
instance instDivisionSemiring [DivisionSemiring K] : DivisionSemiring Kᵒᵈ := ‹_›
Division Semiring Structure on Order Dual
Informal description
For any division semiring $K$, the order dual $K^{\text{op}}$ is also a division semiring.
OrderDual.instDivisionRing instance
[DivisionRing K] : DivisionRing Kᵒᵈ
Full source 
instance instDivisionRing [DivisionRing K] : DivisionRing Kᵒᵈ := ‹_›
Order Dual of a Division Ring is a Division Ring
Informal description
For any division ring $K$, the order dual $K^{\text{op}}$ is also a division ring.
OrderDual.instSemifield instance
[Semifield K] : Semifield Kᵒᵈ
Full source 
instance instSemifield [Semifield K] : Semifield Kᵒᵈ := ‹_›
Order Dual of a Semifield is a Semifield
Informal description
For any semifield $K$, the order dual $K^{\text{op}}$ is also a semifield.
OrderDual.instField instance
[Field K] : Field Kᵒᵈ
Full source 
instance instField [Field K] : Field Kᵒᵈ := ‹_›
Order Dual of a Field is a Field
Informal description
For any field $K$, the order dual $K^{\text{op}}$ is also a field.
toDual_ratCast theorem
[RatCast K] (n : ℚ) : toDual (n : K) = n
Full source 
@[simp] lemma toDual_ratCast [RatCast K] (n : ℚ) : toDual (n : K) = n := rfl
Commutativity of Order Dual with Rational Casting
Informal description
For any type $K$ with a rational casting operation and any rational number $n$, the order dual of the cast of $n$ in $K$ is equal to the cast of $n$ in the order dual of $K$. In other words, the map `toDual` commutes with rational casting: $\text{toDual}(n : K) = n : K^{\text{op}}$.
ofDual_ratCast theorem
[RatCast K] (n : ℚ) : (ofDual n : K) = n
Full source 
@[simp] lemma ofDual_ratCast [RatCast K] (n : ℚ) : (ofDual n : K) = n := rfl
Rational Casting Commutes with Order Dual Conversion
Informal description
For any type $K$ with a rational number casting operation and for any rational number $n$, the element obtained by casting $n$ to the order dual $K^{\text{op}}$ and then applying the `ofDual` map is equal to the element obtained by directly casting $n$ to $K$. In other words, $\text{ofDual}(n : K^{\text{op}}) = n : K$.
Lex.instRatCast instance
[RatCast K] : RatCast (Lex K)
Full source 
instance instRatCast [RatCast K] : RatCast (Lex K) := ‹_›
Rational Casting on Lexicographic Order Type Synonym
Informal description
For any type $K$ equipped with a rational casting operation, the lexicographic order type synonym $\mathsf{Lex}\, K$ also inherits a rational casting operation.
Lex.instDivisionSemiring instance
[DivisionSemiring K] : DivisionSemiring (Lex K)
Full source 
instance instDivisionSemiring [DivisionSemiring K] : DivisionSemiring (Lex K) := ‹_›
Division Semiring Structure on Lexicographic Order
Informal description
For any division semiring $K$, the lexicographic order type synonym $\operatorname{Lex} K$ is also a division semiring.
Lex.instDivisionRing instance
[DivisionRing K] : DivisionRing (Lex K)
Full source 
instance instDivisionRing [DivisionRing K] : DivisionRing (Lex K) := ‹_›
Lexicographic Order Preserves Division Ring Structure
Informal description
For any division ring $K$, the lexicographic order type `Lex K` is also a division ring.
Lex.instSemifield instance
[Semifield K] : Semifield (Lex K)
Full source 
instance instSemifield [Semifield K] : Semifield (Lex K) := ‹_›
Lexicographic Order Preserves Commutative Division Semiring Structure
Informal description
For any commutative division semiring $K$, the lexicographic order on $K$ is also a commutative division semiring.
Lex.instField instance
[Field K] : Field (Lex K)
Full source 
instance instField [Field K] : Field (Lex K) := ‹_›
Lexicographic Order Preserves Field Structure
Informal description
For any field $K$, the lexicographic order type synonym $\mathsf{Lex}\, K$ is also a field with the same algebraic operations as $K$.
toLex_ratCast theorem
[RatCast K] (n : ℚ) : toLex (n : K) = n
Full source 
@[simp] lemma toLex_ratCast [RatCast K] (n : ℚ) : toLex (n : K) = n := rfl
Rational Cast Preservation under Lexicographic Order Equivalence
Informal description
For any type $K$ with a rational casting operation and any rational number $n$, the canonical equivalence `toLex` maps the cast of $n$ in $K$ to the cast of $n$ in the lexicographic order type synonym $\mathsf{Lex}\, K$. That is, $\mathsf{toLex}(n : K) = n : \mathsf{Lex}\, K$.
ofLex_ratCast theorem
[RatCast K] (n : ℚ) : (ofLex n : K) = n
Full source 
@[simp] lemma ofLex_ratCast [RatCast K] (n : ℚ) : (ofLex n : K) = n := rfl
Rational Cast Preservation in Lexicographic Order Conversion
Informal description
For any type $K$ equipped with a rational casting operation and any rational number $n \in \mathbb{Q}$, the conversion from the lexicographic order type synonym $\mathsf{Lex}\, K$ back to $K$ preserves the rational casting operation, i.e., $\mathsf{ofLex}(n) = n$ in $K$.