Units.mk_semiconjBy
theorem Units.mk_semiconjBy : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M), SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
The theorem `Units.mk_semiconjBy` states that for any monoid `M` and any unit `u` and element `x` of `M`, `u` semiconjugates `x` to `u * x * u⁻¹`. In mathematical terminology, this means that the multiplication of `u` and `x` equals the multiplication of `u * x * u⁻¹` and `u`, where `u⁻¹` denotes the multiplicative inverse of `u`. This is a property related to the concept of semiconjugacy in algebraic structures.
More concisely: For any monoid `M` and unit `u` of `M`, `u` semiconjugates `x` if and only if `u * x * u⁻¹ = x`.
|
AddSemiconjBy.addUnits_neg_right
theorem AddSemiconjBy.addUnits_neg_right :
∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M},
AddSemiconjBy a ↑x ↑y → AddSemiconjBy a ↑(-x) ↑(-y)
The theorem `AddSemiconjBy.addUnits_neg_right` states that, for any type `M` that is an additive monoid (a structure with addition operation and an additive identity), if a given element `a` of `M` is an additive semiconjugate of an additive unit `x` to an additive unit `y` (i.e., `a + x = y + a`), then `a` is also an additive semiconjugate of the negative of `x` (`-x`) to the negative of `y` (`-y`) (i.e., `a + (-x) = (-y) + a`). In other words, if `a` semiconjugates `x` to `y`, it also semiconjugates `-x` to `-y`.
More concisely: If `a` is an additive semiconjugate of additive units `x` and `y` in an additive monoid `M`, then `a` is also an additive semiconjugate of `-x` and `-y`. In other words, `a + x = y + a` implies `a + (-x) = (-y) + a`.
|
SemiconjBy.units_inv_right
theorem SemiconjBy.units_inv_right :
∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
The theorem `SemiconjBy.units_inv_right` states that for any type `M` that has a monoid structure, given elements `a`, `x`, and `y` from the group of units of `M`, if `a` semiconjugates `x` to `y` (i.e., if `a * x = y * a`), then `a` also semiconjugates the inverse of `x` to the inverse of `y` (i.e., `a * x⁻¹ = y⁻¹ * a`). Here, `x⁻¹` and `y⁻¹` denote the inverses of `x` and `y` in the group of units.
More concisely: If `a` semiconjugates `x` to `y` in the group of units of a monoid `M`, then `a` semiconjugates the inverses of `x` and `y`, i.e., `a * x⁻¹ = y⁻¹ * a`.
|
AddUnits.mk_addSemiconjBy
theorem AddUnits.mk_addSemiconjBy :
∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M), AddSemiconjBy (↑u) x (↑u + x + ↑(-u))
This theorem states that for any type `M` equipped with an addition operation that forms a monoid, and for any additive unit `u` and element `x` of `M`, `u` semiconjugates `x` to `u + x - u`. In other words, when `u` is added to `x`, it results in the same value as when `u` is added to `u + x - u`. This theorem operates under the assumption of additivity, which is the basic property of a monoid.
More concisely: For any monoid `M` with additive identity `u`, and for all `x` in `M`, `u + x = u + (x + u - u)`.
|
SemiconjBy.units_inv_symm_left
theorem SemiconjBy.units_inv_symm_left :
∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
The theorem `SemiconjBy.units_inv_symm_left` states that for any type `M` equipped with a monoid structure, if a unit `a` semiconjugates `x` to `y`, then the inverse of `a`, denoted `a⁻¹`, semiconjugates `y` to `x`. In other words, if `a * x = y * a` holds, then `a⁻¹ * y = x * a⁻¹` also holds. The concept of semiconjugation is related to the commutative property but applied to different elements.
More concisely: If `a` semiconjugates `x` to `y` in a monoid `M`, then the inverse of `a` semiconjugates `y` to `x`: `a * x = y * a` implies `a⁻¹ * y = x * a⁻¹`.
|
AddSemiconjBy.addUnits_neg_symm_left
theorem AddSemiconjBy.addUnits_neg_symm_left :
∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M},
AddSemiconjBy (↑a) x y → AddSemiconjBy (↑(-a)) y x
This theorem states that if an additive unit `a` semiconjugates `x` to `y`, then the additive inverse of `a`, denoted `-a`, semiconjugates `y` to `x`. In general terms, semiconjugation in this context means that `a + x = y + a`. So if it is true that adding unit `a` to `x` results in the same value as adding `a` to `y`, then adding the negation of `a` to `y` will result in the same value as adding `-a` to `x`. This is within the context of an additive monoid `M`, which is a set equipped with an associative binary operation (in this case, addition) and an identity element (the additive unit).
More concisely: If `a` semiconjugates `x` to `y` in an additive monoid, then `-a` semiconjugates `y` to `x` (i.e., `x + a = y` implies `y + (-a) = x`).
|