isConj_iff_eq
theorem isConj_iff_eq : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, IsConj a b ↔ a = b
This theorem states that for any type `α` that is a commutative monoid, and for any two elements `a` and `b` of `α`, `a` is conjugate to `b` if and only if `a` is equal to `b`. In mathematical terms, the proposition "there exists a unit `c` such that `c * a * c⁻¹ = b`" is equivalent to the proposition "`a` equals `b`".
More concisely: For any commutative monoid type `α`, element equality `(a = b)` is equivalent to the existence of a unit `c` such that `c * a * c⁻¹ = b` (conjugate equality).
|
IsConj.symm
theorem IsConj.symm : ∀ {α : Type u} [inst : Monoid α] {a b : α}, IsConj a b → IsConj b a
The theorem `IsConj.symm` states that for any type `α` that forms a monoid, if an element `a` is conjugate to another element `b` (i.e., there exists a unit `c` such that `c * a * c⁻¹ = b`), then `b` is also conjugate to `a`. This means that conjugacy is a symmetrical relationship in the context of a monoid.
More concisely: If `a` is conjugate to `b` in a monoid, then `b` is conjugate to `a`.
|
ConjClasses.mk_eq_mk_iff_isConj
theorem ConjClasses.mk_eq_mk_iff_isConj :
∀ {α : Type u} [inst : Monoid α] {a b : α}, ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b
The theorem `ConjClasses.mk_eq_mk_iff_isConj` states that for all monoids `α`, and any two elements `a` and `b` from this monoid, the canonical quotient map from `α` into the conjugacy classes of `α` applied to `a` equals the same map applied to `b` if and only if `a` is conjugate to `b`. Here, `a` is considered conjugate to `b` if there exists some unit `c` such that `c * a * c⁻¹ = b`.
More concisely: For all monoids α and elements a, b ∈ α, the canonical quotient map maps a to the same conjugacy class as b if and only if a is conjugate to b.
|
ConjClasses.mem_carrier_iff_mk_eq
theorem ConjClasses.mem_carrier_iff_mk_eq :
∀ {α : Type u} [inst : Monoid α] {a : α} {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
This theorem states that for any type `α` that forms a monoid and any elements `a` in this monoid and `b` in the conjugacy classes of the monoid, the element `a` belongs to the carrier of `b` if and only if the conjugacy class of `a` is equal to `b`. In more mathematical terms, it relates the membership of an element in a particular conjugacy class to the equivalence of the said class to the conjugacy class of the element itself.
More concisely: For any monoid type `α` and elements `a` in `α` and `b` in its conjugacy classes, `a` belongs to the carrier of `b` if and only if `a` and `b` are equal as conjugacy classes.
|
conj_inv
theorem conj_inv : ∀ {α : Type u} [inst : Group α] {a b : α}, (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
This theorem states that for any group `α` and any elements `a` and `b` of `α`, the inverse of the element obtained by multiplying `b`, `a`, and the inverse of `b` in sequence is equal to the sequence obtained by multiplying `b`, the inverse of `a`, and the inverse of `b`. In other words, if you take the product of `b`, `a` and `b⁻¹` and then take the inverse of this product, you get the same result as if you had multiplied `b`, `a⁻¹`, and `b⁻¹` in sequence. This is often referred to as the "conjugate inverse" property in group theory.
More concisely: For any group `α` and elements `a`, `b` in `α`, `b⁻¹ a⁻¹ b = a (b a⁻¹)`.
|
IsConj.refl
theorem IsConj.refl : ∀ {α : Type u} [inst : Monoid α] (a : α), IsConj a a
This theorem states that, for any type `α` that has a monoid structure, any element `a` of that type is conjugate to itself. In other words, for every monoid element `a`, there exists a unit `c` such that `c * a * c⁻¹ = a`. Essentially, this is reflecting that each element in a monoid is conjugate to itself under the relation of conjugacy.
More concisely: For any monoid `α` and its element `a`, there exists a unit `c` in `α` such that `c * a * c⁻¹ = a`.
|
conj_mul
theorem conj_mul : ∀ {α : Type u} [inst : Group α] {a b c : α}, b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹ := by
sorry
This theorem states that for any type `α` that has a group structure, given three elements `a`, `b`, and `c` in `α`, the result of multiplying `b` and `a`, inverting `b`, multiplying the result by `b` and `c`, and inverting `b` again, is equal to the result of multiplying `b` by the product of `a` and `c`, and then inverting `b`. In mathematical terms, this means that for any group, the expression `b * a * b⁻¹ * (b * c * b⁻¹)` is equal to `b * (a * c) * b⁻¹`. This is a statement about the "conjugation" operation in group theory.
More concisely: For any group `α` and elements `a, b, c` in `α`, the conjugation `b * a * b⁻¹` is equivalent to `b * (a * c) * b⁻¹`.
|
IsConj.trans
theorem IsConj.trans : ∀ {α : Type u} [inst : Monoid α] {a b c : α}, IsConj a b → IsConj b c → IsConj a c
The theorem `IsConj.trans` states that for any type `α` that forms a monoid, the conjugacy relationship is transitive. In other words, if for any three elements `a`, `b`, and `c` of the monoid `α`, if `a` is conjugate to `b` and `b` is conjugate to `c`, then `a` is conjugate to `c`. In the language of group theory, if there exists a unit `d` such that `d * a * d⁻¹ = b` and a unit `e` such that `e * b * e⁻¹ = c`, then there must exist a unit `f` such that `f * a * f⁻¹ = c`.
More concisely: If `α` is a monoid and `a`, `b`, and `c` are elements of `α` such that there exist units `d` and `e` in `α` with `d * a * d⁻¹ = b` and `e * b * e⁻¹ = c`, then there exists a unit `f` in `α` with `f * a * f⁻¹ = c`.
|
ConjClasses.forall_isConj
theorem ConjClasses.forall_isConj :
∀ {α : Type u} [inst : Monoid α] {p : ConjClasses α → Prop},
(∀ (a : ConjClasses α), p a) ↔ ∀ (a : α), p (ConjClasses.mk a)
The theorem `ConjClasses.forall_isConj` expresses an equivalence between two predicates in the context of the conjugacy classes of a group. It states that for any type `α` equipped with a monoid structure, a property `p` holding for every conjugacy class of `α` is equivalent to the property `p` holding for every element of `α` when considered as a member of its conjugacy class through the canonical quotient map `ConjClasses.mk`. In other words, we can test a property over all conjugacy classes by testing it simply over all elements of the group.
More concisely: For any monoid `α` and property `p`, `p` holds for all conjugacy classes of `α` if and only if it holds for all elements of `α` viewed as representatives of their conjugacy classes.
|
isConj_iff
theorem isConj_iff : ∀ {α : Type u} [inst : Group α] {a b : α}, IsConj a b ↔ ∃ c, c * a * c⁻¹ = b
This theorem states that for any group `α`, and any elements `a` and `b` of that group, `a` is conjugate to `b` if and only if there exists a unit `c` such that `c * a * c⁻¹ = b`. In the language of group theory, this expresses the property of being conjugate as having a specific form under a group operation.
More concisely: For any group `α` and elements `a, b` in `α`, `a` is conjugate to `b` if and only if there exists a unit `c` in `α` such that `c * a * c⁻¹ = b`.
|