CancelDenoms.sub_subst
theorem CancelDenoms.sub_subst :
∀ {α : Type u_1} [inst : Ring α] {n e1 e2 t1 t2 : α}, n * e1 = t1 → n * e2 = t2 → n * (e1 - e2) = t1 - t2 := by
sorry
This theorem, `CancelDenoms.sub_subst`, states that for any type `α` that forms a ring, and for any elements `n`, `e1`, `e2`, `t1`, `t2` of `α`, if `n` times `e1` equals `t1` and `n` times `e2` equals `t2`, then `n` times the difference `e1 - e2` is equal to the difference `t1 - t2`. In mathematical terms, this theorem is saying that if $n \cdot e1 = t1$ and $n \cdot e2 = t2$, then $n \cdot (e1 - e2) = t1 - t2$. This is a property about distributivity and subtraction in the context of ring theory.
More concisely: For any ring `α` and elements `n`, `e1`, `e2`, `t1`, `t2` in `α`, if `n` times `e1` equals `t1` and `n` times `e2` equals `t2`, then `n` times the difference `e1 - e2` equals the difference `t1 - t2`.
|
CancelDenoms.div_subst
theorem CancelDenoms.div_subst :
∀ {α : Type u_1} [inst : Field α] {n1 n2 k e1 e2 t1 : α},
n1 * e1 = t1 → n2 / e2 = 1 → n1 * n2 = k → k * (e1 / e2) = t1
This theorem states that for any type `α` that is a field, given any elements `n1`, `n2`, `k`, `e1`, `e2`, and `t1` of `α`, if `n1 * e1` equals `t1`, `n2 / e2` equals `1`, and `n1 * n2` equals `k`, then it follows that `k * (e1 / e2)` equals `t1`. This theorem essentially provides a rule for substituting division and multiplication in terms of other product and division expressions, assuming certain conditions are met.
More concisely: If `α` is a field, `n1 * e1 = t1`, `n2 / e2 = 1`, and `n1 * n2 = k`, then `k * (e1 / e2) = t1`.
|
CancelDenoms.derive_trans
theorem CancelDenoms.derive_trans : ∀ {α : Type u_1} [inst : Mul α] {a b c d : α}, a = b → c * b = d → c * a = d := by
sorry
The theorem `CancelDenoms.derive_trans` states that for any type `α` with multiplication operation, given four elements `a`, `b`, `c`, and `d` of that type, if `a` is equal to `b`, and the product of `c` and `b` is equal to `d`, then the product of `c` and `a` is also equal to `d`. This theorem essentially provides a way to chain together equality proofs involving multiplication, allowing for the substitution of equals for equals.
More concisely: If `a = b` and `b * c = d`, then `a * c = d`.
|
CancelDenoms.neg_subst
theorem CancelDenoms.neg_subst : ∀ {α : Type u_1} [inst : Ring α] {n e t : α}, n * e = t → n * -e = -t
This theorem states that for any ring `α`, and any three elements 'n', 'e', and 't' of this ring, if 'n' times 'e' equals 't', then 'n' times the additive inverse of 'e' (i.e., '-e') equals the additive inverse of 't' (i.e., '-t'). Essentially, it asserts that multiplication by a negative element in a ring flips the sign of the product.
More concisely: For any ring `α`, if `n * e = t`, then `n * (-e) = -t`.
|