SemiconjBy.inv_symm_left_iff
theorem SemiconjBy.inv_symm_left_iff :
∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
The theorem `SemiconjBy.inv_symm_left_iff` states that for any group `G` and any elements `a`, `x` and `y` of `G`, the statement "the inverse of `a` is semiconjugate to `y` by `x`" is equivalent to " `a` is semiconjugate to `x` by `y`". Here, an element `a` is said to be semiconjugate to `x` by `y` (denoted as SemiconjBy `a x y`), if the product of `a` and `x` equals the product of `y` and `a`. It's written in mathematical notation as `a * x = y * a`.
More concisely: For any group `G` and elements `a`, `x`, and `y` in `G`, `SemiconjBy x a y` if and only if `SemiconjBy a y x`, where `SemiconjBy a b c` denotes `a * b = c * a`.
|
SemiconjBy.inv_inv_symm_iff
theorem SemiconjBy.inv_inv_symm_iff :
∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
The theorem `SemiconjBy.inv_inv_symm_iff` states that for any division monoid `G` and elements `a`, `x`, and `y` of `G`, `x` is semiconjugate to `y` by `a` inverse if and only if `y` is semiconjugate to `x` by `a`. In terms of the semiconjugate operation, this means that multiplying `a` inverse by `x` inverse equals `y` inverse times `a` inverse if and only if multiplying `a` by `y` equals `x` times `a`. This theorem effectively describes a symmetry property of the semiconjugate relation under taking inverses of the elements.
More concisely: For any division monoid G and elements x, y, and a, x is semiconjugate to y by a if and only if y is semiconjugate to x by a inverse.
|
SemiconjBy.inv_inv_symm
theorem SemiconjBy.inv_inv_symm :
∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a y x → SemiconjBy a⁻¹ x⁻¹ y⁻¹
The theorem `SemiconjBy.inv_inv_symm` states that for any element of a division monoid `G`, if `a`, `x`, and `y` are such that `a` is semiconjugate to `y` by `x` (i.e., `a * x = y * a`), then the inverse of `a` is semiconjugate to the inverse of `x` by the inverse of `y` (i.e., `a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹`). In other words, the semiconjugacy relationship is preserved under inversion of all elements involved.
More concisely: If `a`, `x`, and `y` are elements of a division monoid such that `a` is semiconjugate to `y` by `x` (i.e., `a * x = y * a`), then the inverse of `a` is semiconjugate to the inverse of `x` by the inverse of `y` (i.e., `a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹`).
|
AddSemiconjBy.neg_symm_left_iff
theorem AddSemiconjBy.neg_symm_left_iff :
∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
The theorem `AddSemiconjBy.neg_symm_left_iff` states that for any additively semiconjugate elements `x` and `y` in a given additive group `G` with a mediating element `a`, the negative of `a` is also the mediating element between `y` and `x`. In other words, if `a + x = y + a` then `-a + y = x - a`.
More concisely: If `x` and `y` are additively semiconjugate in an additive group `G` with mediating element `a`, then `-a` is another mediating element between `y` and `x`, i.e., `y = a + x <=> x = a + y <=> a + x = y + a <=> a + y = x + a <=> -a + y = x - a <=> x - a = -a + y`.
|
AddSemiconjBy.neg_neg_symm_iff
theorem AddSemiconjBy.neg_neg_symm_iff :
∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x := by
sorry
The theorem `AddSemiconjBy.neg_neg_symm_iff` states that for any type `G` that forms a subtraction monoid (a type with addition, zero and negation such that addition is associative and each element has an additive inverse), and for any elements `a`, `x`, and `y` in `G`, the statement that `-a` is additive semiconjugate to `-x` by `-y` (which means `-y + -a = -x + -y`) is equivalent to the statement that `a` is additive semiconjugate to `y` by `x` (which means `x + a = y + x`).
More concisely: For any type `G` with add, zero, and negation making it a subtraction monoid, and for any elements `a`, `x`, and `y` in `G`, the subtractions `-a - x = y` and `x + a = y` are equivalent.
|
Mathlib.Algebra.Group.Semiconj.Basic._auxAddLemma.3
theorem Mathlib.Algebra.Group.Semiconj.Basic._auxAddLemma.3 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, `Mathlib.Algebra.Group.Semiconj.Basic._auxAddLemma.3`, states that for any type `α` and any two elements `a` and `b` of this type, the statement "`a` is equal to `b`" is the same as the statement "`b` is equal to `a`". In other words, the theorem asserts the symmetry of equality in any sort or type.
More concisely: The theorem asserts that for all types `α` and elements `a`, `b` of type `α`, the equality `a = b` is equivalent to `b = a`.
|
Mathlib.Algebra.Group.Semiconj.Basic._auxLemma.3
theorem Mathlib.Algebra.Group.Semiconj.Basic._auxLemma.3 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, named `Mathlib.Algebra.Group.Semiconj.Basic._auxLemma.3`, states that for any type `α` and any two objects `a` and `b` of this type, the proposition that `a` is equal to `b` is the same as the proposition that `b` is equal to `a`. In other words, it confirms the symmetry of equality: if `a` equals `b`, then `b` equals `a`, and vice versa.
More concisely: The theorem asserts the reflexivity and symmetry of equality: for all types `α` and objects `a, b` of `α`, `a = b` is equivalent to `b = a`.
|
SemiconjBy.inv_right
theorem SemiconjBy.inv_right : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
The theorem `SemiconjBy.inv_right` states that for any group `G`, given any three elements `a`, `x`, and `y` of `G`, if `a` is semiconjugate to `y` by `x` (meaning `x * a = y * x`), then `a` is also semiconjugate to the inverse of `y` by the inverse of `x`. In mathematical terms, if `x * a = y * x`, then `x⁻¹ * a = y⁻¹ * x⁻¹`.
More concisely: If `x` semiconjugates `a` to `y` in a group `G`, then `x^{-1}` semiconjugates `a` to `y^{-1}`.
|
SemiconjBy.inv_symm_left
theorem SemiconjBy.inv_symm_left :
∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
This theorem, known as `SemiconjBy.inv_symm_left`, says that for any group `G` and elements `a`, `x`, and `y` of this group, if `a` is semiconjugate to `x` by `y` (i.e., `a * x = y * a`), then `a⁻¹` (the inverse of `a`) is semiconjugate to `y` by `x` (i.e., `a⁻¹ * y = x * a⁻¹`). This is an alias for the reverse direction of another theorem, `SemiconjBy.inv_symm_left_iff`.
More concisely: If `a` is semiconjugate to `x` by `y` in a group, then `a^{-1}` is semiconjugate to `y` by `x`.
|