AddSemiconjBy.conj_mk
theorem AddSemiconjBy.conj_mk : ∀ {G : Type u_3} [inst : AddGroup G] (a x : G), AddSemiconjBy a x (a + x + -a) := by
sorry
The theorem `AddSemiconjBy.conj_mk` states that for any additive group `G` and any elements `a` and `x` in `G`, `a` is an additive semiconjugate between `x` and `a + x + -a`. In other words, for any two elements in an additive group, we can always find a third element that satisfies the property of additive semiconjugation, where the semiconjugate of `x` is `a + x + -a`.
More concisely: For any additive group G and elements a, x in G, a is an additive semiconjugate of x if and only if x = a + x + (-a).
|
AddSemiconjBy.eq
theorem AddSemiconjBy.eq : ∀ {S : Type u_1} [inst : Add S] {a x y : S}, AddSemiconjBy a x y → a + x = y + a
The theorem `AddSemiconjBy.eq` states that for any type `S` with addition (`Add`), given elements `a`, `x`, and `y` of `S`, if `x` is additive semiconjugate to `y` by `a` (i.e., `AddSemiconjBy a x y` holds true), then the sum of `a` and `x` equals the sum of `y` and `a`. This theorem is useful for rewriting expressions in Lean 4.
More concisely: For any type `S` with addition, if `x` is additive semiconjugate to `y` by `a` (i.e., `x = a + y`), then `a + x = y + a`.
|
SemiconjBy.reflexive
theorem SemiconjBy.reflexive : ∀ {M : Type u_2} [inst : MulOneClass M], Reflexive fun a b => ∃ c, SemiconjBy c a b := by
sorry
The theorem `SemiconjBy.reflexive` states that the relation "there exists an element that semiconjugates `a` to `b`" is reflexive on any type `M` that is a monoid or, more generally, a `MulOneClass`. This means that for every element `a` in `M` there exists an element (specifically, the multiplicative identity `1`) that semiconjugates `a` to itself, i.e., `1 * a = a * 1`. In other words, every element in the monoid is semiconjugate to itself by the multiplicative identity.
More concisely: For every element `a` in a monoid or `MulOneClass` type `M`, the multiplicative identity `1` semiconjugates `a` to itself, i.e., `1 * a = a * 1`.
|
AddSemiconjBy.add_left
theorem AddSemiconjBy.add_left :
∀ {S : Type u_1} [inst : AddSemigroup S] {a b x y z : S},
AddSemiconjBy a y z → AddSemiconjBy b x y → AddSemiconjBy (a + b) x z
The theorem `AddSemiconjBy.add_left` states that for any type `S` equipped with an addition operation, and for any elements `a`, `b`, `x`, `y`, and `z` of this type, if `b` is an additive semiconjugate from `x` to `y` and `a` is an additive semiconjugate from `y` to `z`, then `a + b` is an additive semiconjugate from `x` to `z`. In other words, if `b + x = y + b` and `a + y = z + a`, then `(a + b) + x = z + (a + b)`. This theorem shows a kind of transitivity property for the relation of being an additive semiconjugate.
More concisely: If `a` is an additive semiconjugate from `y` to `z` and `b` is an additive semiconjugate from `x` to `y`, then `a + b` is an additive semiconjugate from `x` to `z`.
|
AddSemiconjBy.reflexive
theorem AddSemiconjBy.reflexive :
∀ {M : Type u_2} [inst : AddZeroClass M], Reflexive fun a b => ∃ c, AddSemiconjBy c a b
This theorem states that in any additive monoid (or, more generally, in any `AddZeroClass` type), the relation "there exists an element that semiconjugates `a` to `b`" is reflexive. In other words, for any element in such a type, there exists another element that satisfies the condition of being an additive semiconjugate, meaning that it can be added to the first element to yield the same result as adding it to itself. This is a statement about the structure of these types, asserting a particular kind of symmetry property.
More concisely: In any AddMonoid (additive monoid or AddZeroClass type), the relation "there exists an element that semiconjugates a to b" is reflexive, i.e., for all a, there exists an element x such that a + x = a.
|
SemiconjBy.transitive
theorem SemiconjBy.transitive : ∀ {S : Type u_1} [inst : Semigroup S], Transitive fun a b => ∃ c, SemiconjBy c a b := by
sorry
This theorem states that within any semigroup, the relation "there exists an element that semiconjugates `a` to `b`" is transitive. In other words, for any elements `a`, `b`, and `c` in the semigroup, if there exists an element that semiconjugates `a` to `b` and there exists another element that semiconjugates `b` to `c`, then there also exists an element that semiconjugates `a` to `c`. Here, semiconjugation is defined as `x` being semiconjugate to `y` by `a` if `a * x = y * a`, where `*` is the multiplication operation of the semigroup.
More concisely: In any semigroup, if there exist elements `a, b, c` such that `a * x = b * a` and `a * y = c * a` for some `x` and `y`, then there exists an element `z` such that `a * z = c * a`.
|
SemiconjBy.one_right
theorem SemiconjBy.one_right : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
The theorem `SemiconjBy.one_right` states that for any type `M` which possesses a multiplication operation and a multiplicative identity element (`1`), every element `a` of `M` semiconjugates `1` to `1`. In other words, for any element `a` in `M`, the product `a * 1` is equal to `1 * a`, which is essentially the definition of a multiplicative identity.
More concisely: For any type `M` with multiplication and multiplicative identity `1`, every element `a` in `M` satisfies `a * 1 = 1 * a`.
|
SemiconjBy.mul_left
theorem SemiconjBy.mul_left :
∀ {S : Type u_1} [inst : Semigroup S] {a b x y z : S},
SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
The theorem `SemiconjBy.mul_left` states that in a semigroup `S`, if `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then the product of `a` and `b` semiconjugates `x` to `z`. In other words, if `b * x = y * b` and `a * y = z * a`, then `(a * b) * x = z * (a * b)`. This asserts a sort of transitivity property for the semiconjugation relation in the context of semigroups.
More concisely: In a semigroup, if elements `x`, `y`, `z`, `a`, and `b` satisfy `b * x = y * b` and `a * y = z * a`, then `(a * b) * x = z * (a * b)`.
|
AddSemiconjBy.transitive
theorem AddSemiconjBy.transitive :
∀ {S : Type u_1} [inst : AddSemigroup S], Transitive fun a b => ∃ c, AddSemiconjBy c a b
This theorem states that in an additive semigroup, the relation "there exists an element that semiconjugates `a` to `b`" is transitive. This means that if there exists an element `c` such that `c` semiconjugates `a` to `b` (i.e. `c + a = b + c`), and there exists an element `d` such that `d` semiconjugates `b` to `e` (i.e. `d + b = e + d`), then there exists an element `f` that semiconjugates `a` to `e` (i.e. `f + a = e + f`). In other words, the existence of a semiconjugating element is a property that passes along a chain of such relations.
More concisely: In an additive semigroup, if there exist elements `c` and `d` such that `c + a = b + c` and `d + b = e + d`, then there exists an element `f` such that `f + a = e + f`.
|
SemiconjBy.pow_right
theorem SemiconjBy.pow_right :
∀ {M : Type u_2} [inst : Monoid M] {a x y : M}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (x ^ n) (y ^ n) := by
sorry
The theorem `SemiconjBy.pow_right` states that for any type `M` that forms a monoid, and given any three elements `a`, `x`, and `y` from `M`, if `a` is semiconjugate to `x` by `y` (i.e., `a * x = y * a`), then for any natural number `n`, `a` is also semiconjugate to `x^n` by `y^n` (i.e., `a * x^n = y^n * a`). In other words, the property of being semiconjugate is preserved under exponentiation.
More concisely: If `a`, `x`, and `y` are in a monoid `M` with `a` semiconjugate to `x` by `y` (i.e., `a * x = y * a`), then for any natural number `n`, `a` is semiconjugate to `x^n` by `y^n` (i.e., `a * x^n = y^n * a`).
|
SemiconjBy.one_left
theorem SemiconjBy.one_left : ∀ {M : Type u_2} [inst : MulOneClass M] (x : M), SemiconjBy 1 x x
This theorem states that for any type `M` equipped with a multiplication and a `1` (an instance of `MulOneClass`), any element `x` of type `M` is semiconjugate to itself by `1`. In mathematical terms, this means that `1 * x = x * 1` for any `x`, which is a property of the multiplicative identity in a multiplicative monoid or a similar algebraic structure.
More concisely: For any type `M` with a multiplication and `1` (`MulOneClass`), the multiplicative identity `1` commutes with any element `x` in `M`, i.e., `1 * x = x * 1`.
|
AddSemiconjBy.add_right
theorem AddSemiconjBy.add_right :
∀ {S : Type u_1} [inst : AddSemigroup S] {a x y x' y' : S},
AddSemiconjBy a x y → AddSemiconjBy a x' y' → AddSemiconjBy a (x + x') (y + y')
The theorem `AddSemiconjBy.add_right` states that for any type `S` equipped with an addition operation (`AddSemigroup S`), if a semiconjugates `x` to `y` and `x'` to `y'`, then `a` also semiconjugates the sum `x + x'` to `y + y'`. In other words, if `a + x = y + a` and `a + x' = y' + a`, then `a + (x + x') = (y + y') + a`. This theorem extends the property of semiconjugation by addition to the sum of two elements.
More concisely: If `a` semiconjugates `x` to `y` and `x'` to `y'`, then `a` semiconjugates `x + x'` to `y + y'`.
|
SemiconjBy.eq
theorem SemiconjBy.eq : ∀ {S : Type u_1} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
The theorem `SemiconjBy.eq` states that for any type `S` with a multiplication operation, given elements `a`, `x` and `y` of `S`, if `x` is semiconjugate to `y` by `a` (which is defined as `a * x = y * a`), then the equation `a * x = y * a` holds true. This theorem is particularly useful for rewriting expressions in proofs involving semiconjugacy.
More concisely: If `a`, `x`, and `y` are elements of a type `S` with a multiplication operation, and `x` is semiconjugate to `y` by `a` (i.e., `a * x = y * a`), then `a * x = y * a`.
|
AddSemiconjBy.zero_left
theorem AddSemiconjBy.zero_left : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : M), AddSemiconjBy 0 x x
This theorem declares that zero semiconjugates any element to itself. In other words, if we have an additive structure with a zero element in a certain type, then for any element 'x' of this type, the sum of zero and 'x' equals the sum of 'x' and zero. Essentially, it encapsulates the property of zero in addition, where zero added to any element does not change the value of that element.
More concisely: For any additive structure with a zero element, zero is an identity element for addition, i.e., for all x, x + 0 = 0 + x.
|
AddSemiconjBy.zero_right
theorem AddSemiconjBy.zero_right : ∀ {M : Type u_2} [inst : AddZeroClass M] (a : M), AddSemiconjBy a 0 0
The theorem `AddSemiconjBy.zero_right` states that for any type `M` that has an addition operation and a zero element, any element `a` of type `M` semiconjugates `0` to `0`. In other words, for any element `a` in `M`, the equation `a + 0 = 0 + a` always holds true. This captures the property that adding zero to any element in an additive structure does not change its value.
More concisely: For any additive type `M` and any element `a` in `M`, `a + 0 = 0 + a`.
|
SemiconjBy.mul_right
theorem SemiconjBy.mul_right :
∀ {S : Type u_1} [inst : Semigroup S] {a x y x' y' : S},
SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')
This theorem states that if a element `a` of a semigroup `S` semiconjugates two pairs of elements `(x, y)` and `(x', y')`, i.e., `a * x = y * a` and `a * x' = y' * a`, then `a` also semiconjugates the product of these pairs `(x * x', y * y')`. In other words, if the multiplication of `a` and `x` changes the order of multiplication with respect to `y`, and the same holds for `x'` and `y'`, then the same property holds for the products `x * x'` and `y * y'`.
More concisely: If `a` semiconjugates `(x, y)` and `(x', y')` in a semigroup `S`, then `a` semiconjugates their product `(x * x', y * y')`.
|
SemiconjBy.conj_mk
theorem SemiconjBy.conj_mk : ∀ {G : Type u_3} [inst : Group G] (a x : G), SemiconjBy a x (a * x * a⁻¹)
The theorem `SemiconjBy.conj_mk` states that for any group `G`, and any elements `a` and `x` in `G`, `a` semiconjugates `x` to `a * x * a⁻¹`. In mathematical terms, this means that the multiplication of `a` and `x` equals the multiplication of `a * x * a⁻¹` and `a` (`a * x = a * x * a⁻¹ * a`). This is a property about the relationship between two elements in a group modulated by a third one.
More concisely: For any group `G` and elements `a, x ∈ G`, `a * x = a * x * a⁻¹ * a`.
|