AddOpposite.addSemiconjBy_op
theorem AddOpposite.addSemiconjBy_op :
∀ {α : Type u_1} [inst : Add α] {a x y : α},
AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x) ↔ AddSemiconjBy a x y
The theorem `AddOpposite.addSemiconjBy_op` states that for any type `α` equipped with addition (`Add α`), and for any elements `a`, `x`, and `y` of `α`, the element `a` is additive semiconjugate to `x` by `y` if and only if the additive opposite of `a` is additive semiconjugate to the additive opposite of `x` by the additive opposite of `y`. In mathematical terms, `a + x = y + a` if and only if `-a + -x = -y + -a`.
More concisely: For all types `α` with addition and elements `a`, `x`, `y` in `α`, `a` is additive semiconjugate to `x` by `y` if and only if the additive opposite of `a` is additive semiconjugate to the additive opposite of `x` by the additive opposite of `y`. In symbols, `a + x = y + a` if and only if `-a + -x = -y + -a`.
|
MulOpposite.semiconjBy_op
theorem MulOpposite.semiconjBy_op :
∀ {α : Type u_1} [inst : Mul α] {a x y : α},
SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x) ↔ SemiconjBy a x y
The theorem `MulOpposite.semiconjBy_op` states that for any type `α` equipped with a multiplication operation, and for any elements `a`, `x`, `y` of this type, `a` is semiconjugate to `x` by `y` if and only if the MulOpposite of `a` is semiconjugate to the MulOpposite of `y` by the MulOpposite of `x`. Semiconjugacy is defined here as `a` times `x` being equal to `y` times `a`. In other words, the theorem establishes an equivalence between the semiconjugacy relations of elements and their MulOpposite counterparts.
More concisely: For any type equipped with multiplication and elements `a`, `x`, `y`, `a` is semiconjugate to `x` by `y` if and only if the MulOpposite of `a` is semiconjugate to the MulOpposite of `y` by the MulOpposite of `x` (i.e., `a * x = y * a` if and only if `-a * -x = -y * -a`).
|
AddMonoidHom.mul_op_ext
theorem AddMonoidHom.mul_op_ext :
∀ {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f g : αᵐᵒᵖ →+ β),
f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom → f = g
The theorem `AddMonoidHom.mul_op_ext` states that for any types `α` and `β` which have `AddZeroClass` structures (that is, they have addition and zero operations that satisfy the appropriate laws), if you have two additive monoid homomorphisms (`f` and `g`) from the multiplicative opposite of `α` to `β`, then the equality of their composition with the additive monoid homomorphism `MulOpposite.opAddEquiv.toAddMonoidHom` implies the equality of `f` and `g` themselves. This is useful because there may be extensionality lemmas for specific types `α` that apply to an equality of `α →+ β`, such as `Finsupp.addHom_ext'`.
More concisely: If `f` and `g` are additive monoid homomorphisms from the multiplicative opposite of type `α` to type `β`, where `α` and `β` have `AddZeroClass` structures, then the equality of their compositions with `MulOpposite.opAddEquiv.toAddMonoidHom` implies the equality of `f` and `g`.
|
IsUnit.op
theorem IsUnit.op : ∀ {M : Type u_2} [inst : Monoid M] {m : M}, IsUnit m → IsUnit (MulOpposite.op m)
This theorem states that for any type `M` that forms a `Monoid`, if an element `m` of `M` is a unit (i.e., it has a two-sided inverse), then the corresponding element of the Multiplicative Opposite `Mᵐᵒᵖ` (obtained using the `MulOpposite.op` function) is also a unit. In other words, the property of being a unit is preserved under the operation of taking multiplicative opposites.
More concisely: If `M` is a monoid and `m` in `M` is a unit, then the multiplicative opposite of `m` is also a unit.
|