SemiconjBy.neg_right
theorem SemiconjBy.neg_right :
∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy a (-x) (-y)
The theorem `SemiconjBy.neg_right` states that for any type `R` which supports multiplication and distribution of negative sign over multiplication, and for any elements `a`, `x`, and `y` of `R`, if `x` is semiconjugate to `y` by `a` (that is, if `a * x = y * a`), then `-x` is semiconjugate to `-y` by `a` (that is, `a * (-x) = (-y) * a`). In other words, if `a * x = y * a`, then it follows that `a * (-x) = (-y) * a`.
More concisely: If `a`, `x`, and `y` are elements of a type `R` with multiplication and distributivity of negative signs, and `x` is semiconjugate to `y` by `a`, then `-x` is semiconjugate to `-y` by `a`. In other words, `a * (-x) = (-y) * a` given `a * x = y * a`.
|
SemiconjBy.neg_left
theorem SemiconjBy.neg_left :
∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy (-a) x y := by
sorry
The theorem `SemiconjBy.neg_left` states that for any type `R` that has a multiplication operation (`Mul R`) and a distributable negation operation (`HasDistribNeg R`), and for any three elements `a`, `x`, and `y` of this type `R`, if `a` is semiconjugate to `y` by `x` (i.e., `a * x = y * a`), then `-a` (the negation of `a`) is also semiconjugate to `y` by `x` (i.e., `-a * x = y * -a`). This theorem captures a property of semiconjugacy under negation in the context of multiplication in a ring (or similar mathematical structure).
More concisely: If `a`, `x`, and `y` are elements of a type `R` with multiplication and distributive negation, and `a` is semiconjugate to `y` by `x`, then `-a` is semiconjugate to `y` by `x`.
|