neg_inv
theorem neg_inv : ∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] {a : K}, -a⁻¹ = (-a)⁻¹ := by
sorry
This theorem, `neg_inv`, states that for any type `K` (where `K` is a division monoid and has the property of distributive negation) and for any instance `a` of type `K`, the inverse of the negative of `a` is equal to the negative of the inverse of `a`. In mathematical terms, this can be represented as `-a⁻¹ = (-a)⁻¹`. This theorem is a demonstration of the property of negation in relation to inversion in a division monoid.
More concisely: For any division monoid `K` and element `a` of type `K` with distributive negation, the inverse of the negative of `a` equals the negative of the inverse of `a`: `-a⁻¹ = (-a)⁻¹`.
|
add_div'
theorem add_div' : ∀ {α : Type u_1} [inst : DivisionSemiring α] (a b c : α), c ≠ 0 → b + a / c = (b * c + a) / c := by
sorry
This theorem states that for any type `α` that forms a division semiring, and for any three elements `a`, `b`, and `c` of type `α`, as long as `c` is not zero, the sum of `b` and `a` divided by `c` is equal to the result of `b` times `c` plus `a`, all divided by `c`. In mathematical terms, it is asserting that for all `a`, `b`, `c` in a division semiring `α`, given `c ≠ 0`, it holds that `b + a / c = (b * c + a) / c`.
More concisely: For any division semiring `α` and elements `a, b, c` in `α` with `c neq 0`, `b + a / c = (b * c + a) / c`.
|
sub_div
theorem sub_div : ∀ {K : Type u_3} [inst : DivisionRing K] (a b c : K), (a - b) / c = a / c - b / c
This theorem states that for any division ring `K` and any three elements `a`, `b`, and `c` of `K`, the operation of subtracting `b` from `a` and then dividing by `c` is equivalent to first dividing `a` and `b` by `c` separately and then subtracting the results. In LaTeX mathematics terms, it can be shown as: for all `a`, `b`, `c` in `K`, `(a - b) / c = a / c - b / c`.
More concisely: For any division ring `K` and elements `a`, `b`, `c` in `K`, the expression `(a - b) / c` is equivalent to `(a / c) - (b / c)`.
|
div_neg
theorem div_neg :
∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] {b : K} (a : K), a / -b = -(a / b)
This theorem states that for any type `K` that forms a division monoid and supports the distribution of negation, the division of an element `a` by the negation of an element `b` is equal to the negation of the division of `a` by `b`. In mathematical terms, it's asserting that `a / -b = -(a / b)` for all elements `a` and `b` in `K`.
More concisely: For any type `K` that forms a division monoid and supports the distribution of negation, the division of an element by the negation of another element is equal to the negation of their quotient: `a / -b = -(a / b)`.
|
Commute.div_add_div
theorem Commute.div_add_div :
∀ {α : Type u_1} [inst : DivisionSemiring α] {a b c d : α},
Commute b c → Commute b d → b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + b * c) / (b * d)
The theorem `Commute.div_add_div` states that for any division semiring `α` and any elements `a`, `b`, `c`, and `d` of `α`, if `b` commutes with `c` and `b` also commutes with `d`, and both `b` and `d` are non-zero, then the value of the sum `a / b + c / d` is equal to `(a * d + b * c) / (b * d)`. In mathematical terms, this says that for elements in a division semiring where multiplication is commutative for certain pairs, the sum of two fractions equals the fraction whose numerator is the sum of the cross products of the numerators and denominators of the original fractions, and whose denominator is the product of the original denominators.
More concisely: For any division semiring with commutative multiation, and for non-zero elements a, b, c, and d such that b commutes with both c and d, we have a / b + c / d = (a * d + b * c) / (b * d).
|
add_div
theorem add_div : ∀ {α : Type u_1} [inst : DivisionSemiring α] (a b c : α), (a + b) / c = a / c + b / c
This theorem, named `add_div`, states that for any type `α` which is a DivisionSemiring, and for any three elements `a`, `b`, and `c` of this type, the operation of dividing the sum of `a` and `b` by `c` is equivalent to the sum of `a` divided by `c` and `b` divided by `c`. In mathematical notations, it states that $(a + b) / c = a / c + b / c$ for all `a`, `b`, and `c` in type `α`. This theorem captures the fact that division distributes over addition in a DivisionSemiring.
More concisely: In a DivisionSemiring, the division of the sum of two elements by a third element is equivalent to the sum of their individual divisions by that element. $(a + b) / c = a / c + b / c$ for all $a, b, c$ in the type $\alpha$.
|
div_sub_div
theorem div_sub_div :
∀ {K : Type u_3} [inst : Field K] (a : K) {b : K} (c : K) {d : K},
b ≠ 0 → d ≠ 0 → a / b - c / d = (a * d - b * c) / (b * d)
This theorem states that for any field `K` and any elements `a`, `b`, `c`, `d` of `K` where `b` and `d` are not zero, the difference between the fraction `a / b` and the fraction `c / d` is equal to the fraction whose numerator is the difference of the product of `a` and `d` and the product of `b` and `c`, and whose denominator is the product of `b` and `d`. In mathematical notation, this would be expressed as $\frac{a}{b} - \frac{c}{d} = \frac{a*d - b*c}{b*d}$, assuming $b \neq 0$ and $d \neq 0$.
More concisely: The difference of fractions $\frac{a}{b}$ and $\frac{c}{d}$ is equal to the fraction $\frac{a\cdot d - b\cdot c}{b\cdot d}$, provided $b \neq 0$ and $d \neq 0$.
|
RingHom.injective
theorem RingHom.injective :
∀ {α : Type u_1} {β : Type u_2} [inst : DivisionRing α] [inst_1 : Semiring β] [inst_2 : Nontrivial β] (f : α →+* β),
Function.Injective ⇑f
The theorem `RingHom.injective` states that for any two types `α` and `β`, if `α` is a division ring (a type of algebraic structure), `β` is a semiring (another type of algebraic structure), and `β` is non-trivial (i.e., it contains at least two distinct elements), then any ring homomorphism `f` from `α` to `β` is injective. In other words, if `f a1` and `f a2` are equal for some elements `a1` and `a2` in `α`, then `a1` and `a2` must be the same element.
More concisely: If `α` is a division ring and `β` is a non-trivial semiring, then every ring homomorphism from `α` to `β` is injective.
|
neg_div_neg_eq
theorem neg_div_neg_eq :
∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] (a b : K), -a / -b = a / b
This theorem states that for any type `K` that is a division monoid and has a distributive negation operation, the division of the negation of `a` by the negation of `b` equals the division of `a` by `b`. In mathematical terms, this can be expressed as: for all `a` and `b` in `K`, `-a / -b = a / b`.
More concisely: For any division monoid `K` with distributive negation, `-a / -b = a / b` for all `a, b` in `K`.
|
div_add_div_same
theorem div_add_div_same : ∀ {α : Type u_1} [inst : DivisionSemiring α] (a b c : α), a / c + b / c = (a + b) / c := by
sorry
This theorem, `div_add_div_same`, states that for any type `α` that is a Division Semiring, the sum of two numbers `a` and `b` divided by a third number `c` is equivalent to the sum of `a` divided by `c` and `b` divided by `c`. In mathematical terms, it asserts that for all `a`, `b`, and `c` in a Division Semiring `α`, the equation $\frac{a}{c} + \frac{b}{c} = \frac{a + b}{c}$ holds.
More concisely: For any division semigroup `α`, the expression `(a / c) + (b / c)` is equal to `(a + b) / c`.
|
sub_div'
theorem sub_div' : ∀ {K : Type u_3} [inst : Field K] (a b c : K), c ≠ 0 → b - a / c = (b * c - a) / c
This theorem states that for any type `K` which is a field, given any three elements `a`, `b`, and `c` of type `K`, where `c` is not equal to zero, the value of the expression `b - a / c` is equal to `(b * c - a) / c`. Essentially, this theorem rearranges a subtraction and division operation into a single division operation.
More concisely: For any field `K` and elements `a`, `b`, and `c` in `K` with `c` non-zero, `b - a / c` equals `(b * c - a) / c`.
|
neg_div'
theorem neg_div' : ∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] (a b : K), -(b / a) = -b / a
This theorem, `neg_div'`, states that for any type `K` that is a division monoid and has a distributive negation property, for any two elements `a` and `b` of `K`, the negation of the result of dividing `b` by `a` is equal to the result of dividing the negation of `b` by `a`. In mathematical terms, this can be written as: for all `a` and `b` in `K`, `- (b / a) = -b / a`.
More concisely: For any type `K` with a distributive negation property and division monoid structure, the negation of the quotient of two elements is equal to the quotient of their negations: `- (b / a) = -b / a`.
|
div_sub'
theorem div_sub' : ∀ {K : Type u_3} [inst : Field K] (a b c : K), c ≠ 0 → a / c - b = (a - c * b) / c
This theorem states that for any field `K` and any elements `a`, `b`, and `c` of `K`, such that `c` is not zero, the expression `a / c - b` is equal to `(a - c * b) / c`. This essentially gives us a formula to simplify division and subtraction in a field.
More concisely: For any field `K` and elements `a`, `b`, and `c` in `K` with `c ≠ 0`, we have `(a / c - b) = (a - c * b) / c`.
|
inv_neg
theorem inv_neg : ∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] {a : K}, (-a)⁻¹ = -a⁻¹ := by
sorry
This theorem, `inv_neg`, states that for any type `K` that is a division monoid and supports distributed negation, the inverse of the negation of any element `a` from `K` is equal to the negative of the inverse of `a`. In mathematical terms, it asserts that `(-a)⁻¹ = -a⁻¹` for all `a` in `K`.
More concisely: For any type `K` being a division monoid with distributed negation, the inverse of the negation of an element `a` equals the negation of the inverse of `a`: `(-a)⁻¹ = -a⁻¹`.
|
one_sub_div
theorem one_sub_div : ∀ {K : Type u_3} [inst : DivisionRing K] {a b : K}, b ≠ 0 → 1 - a / b = (b - a) / b
This theorem, named `one_sub_div`, applies to any division ring `K` and two elements `a` and `b` in `K`. It states that, assuming `b` is not equal to zero, subtracting `a / b` from `1` is equivalent to dividing the difference of `b` and `a` by `b`. In mathematical terms, it asserts that:
1 - (a / b) = (b - a) / b, given that b ≠ 0.
More concisely: Given a division ring `K` and elements `a, b` in `K` with `b ≠ 0`, the equality `1 - (a / b) = (b - a) / b` holds.
|
div_add_div
theorem div_add_div :
∀ {α : Type u_1} [inst : Semifield α] {b d : α} (a c : α),
b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + b * c) / (b * d)
This theorem states that for any type `α` that forms a Semifield, given non-zero elements `b` and `d` of this type and any elements `a` and `c`, the sum of the division of `a` by `b` and the division of `c` by `d` is equal to the division of the sum of `a` multiplied by `d` and `b` multiplied by `c` by the product of `b` and `d`. In mathematical terms, it's saying that for all `a`, `b`, `c`, `d` in a Semifield where `b` and `d` are not zero, the equation $\frac{a}{b} + \frac{c}{d} = \frac{a \cdot d + b \cdot c}{b \cdot d}$ holds.
More concisely: For any semifield `α` with non-zero elements `b` and `d`, the sum of the quotients of `a` by `b` and `c` by `d` equals the quotient of the product of `a` multiplied by `d` and `b` multiplied by `c` by the product of `b` and `d`. In symbols: $\frac{a}{b} + \frac{c}{d} = \frac{a \cdot d + b \cdot c}{b \cdot d}$.
|
inv_sub_inv'
theorem inv_sub_inv' :
∀ {K : Type u_3} [inst : DivisionRing K] {a b : K}, a ≠ 0 → b ≠ 0 → a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
This is a theorem about the subtraction of two inverses in a division ring. Specifically, for any division ring `K` and any two non-zero elements `a` and `b` of `K`, the difference of the inverses of `a` and `b` is equal to the inverse of `a` times the difference of `b` and `a`, all multiplied by the inverse of `b`. This theorem is more convenient to use when `K` is a commutative division ring, in which case refer to the theorem `inv_sub_inv`.
More concisely: For any commutative division ring `K` and non-zero elements `a` and `b` of `K`, the inverse of `(b - a)` is equal to `(b^(-1) * a^(-1)) * (b - a)`.
|
div_sub_div_same
theorem div_sub_div_same : ∀ {K : Type u_3} [inst : DivisionRing K] (a b c : K), a / c - b / c = (a - b) / c
This theorem states that for any division ring `K` and for any elements `a`, `b`, and `c` in `K`, the difference between `a` divided by `c` and `b` divided by `c` is equal to the result of `a` minus `b` divided by `c`. In mathematical expression, it can be written as: $\frac{a}{c} - \frac{b}{c} = \frac{a-b}{c}$.
More concisely: For any division ring K and elements a, b, and c in K, $\frac{a}{c} - \frac{b}{c} = \frac{a-b}{c}$.
|
one_div_neg_one_eq_neg_one
theorem one_div_neg_one_eq_neg_one :
∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K], 1 / -1 = -1
This theorem states that in any division monoid `K` that also supports the distribution of negation over multiplication and addition, the division of 1 by -1 always equates to -1. A division monoid is a structure with a single binary operation that is associative and has an identity element, and every element has a multiplicative inverse. The distribution of negation means that negating a sum of two elements is the same as summing their negations.
More concisely: In a division monoid with negation distribution, the multiplicative inverse of 1 is -1.
|
neg_div
theorem neg_div : ∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] (a b : K), -b / a = -(b / a)
The theorem `neg_div` states that for any type `K` which is a division monoid and has distributive negation, the negation of the division of `b` by `a` is the same as the division of the negation of `b` by `a`. In mathematical terms, it says that $-\frac{b}{a} = -(\frac{b}{a})$ for all `a` and `b` in `K`.
More concisely: For any division monoid `K` with distributive negation, $-(b/a) = (-\ b)/a$.
|
div_neg_eq_neg_div
theorem div_neg_eq_neg_div :
∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] (a b : K), b / -a = -(b / a)
This theorem states that for any division monoid `K` that also supports negation, and for any two elements `a` and `b` in `K`, the result of dividing `b` by `-a` is the same as the negative of dividing `b` by `a`. In mathematical notation, it says that for all `a` and `b` in `K`, `b / -a = -(b / a)`.
More concisely: For any division monoid `K` with negation, the quotient of an element by its additive inverse equals the additive inverse of the quotient: `b / -a = -(b / a)`.
|