Mathlib.GroupTheory.GroupAction.ConjAct._auxLemma.2
theorem Mathlib.GroupTheory.GroupAction.ConjAct._auxLemma.2 :
∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem states that for any proposition `b` and any type `α` such that `α` is nonempty (there exists at least one element of type `α`), the type of functions from `α` to `b` is equal to `b`. In other words, when `α` is nonempty, the type of functions from `α` to a given proposition is essentially the same as that proposition itself.
More concisely: For any nonempty type `α`, the type of functions from `α` to a proposition `b` is equivalent to `b`.
|
ConjAct.smul_def
theorem ConjAct.smul_def :
∀ {G : Type u_3} [inst : DivInvMonoid G] (g : ConjAct G) (h : G),
g • h = ConjAct.ofConjAct g * h * (ConjAct.ofConjAct g)⁻¹
The theorem `ConjAct.smul_def` states that for any group `G` with division and inversion (given by the typeclass `DivInvMonoid G`), and for any elements `g` in `ConjAct G` and `h` in `G`, the action of `g` on `h` (denoted as `g • h`) is equal to the conjugation of `h` by `g`. In this context, conjugation is given by the product of `g`, `h` and the inverse of `g` in that order, i.e., `g * h * g⁻¹`, where `g⁻¹` is the inverse of `g`. This action is referred to as the "conjugation action" of `g` on `h`.
More concisely: For any group with division and inversion, the action of an element on another element is equal to their conjugation, that is, the product of the element, the second element, and the inverse of the first element.
|
Mathlib.GroupTheory.GroupAction.ConjAct._auxLemma.1
theorem Mathlib.GroupTheory.GroupAction.ConjAct._auxLemma.1 :
∀ {G : Type u_3} [inst : DivInvMonoid G] (p : ConjAct G → Prop),
(∀ (x : ConjAct G), p x) = ∀ (x : G), p (ConjAct.toConjAct x)
This theorem states that for any type `G` with an instance of `DivInvMonoid` (a type of group), and any property `p` defined on the action of the group `G` on itself by conjugation (`ConjAct G`), the property `p` holds for all elements of `ConjAct G` if and only if it holds for all elements `x` of `G` under the `ConjAct.toConjAct` map. This essentially means that the property `p` is preserved under the action of conjugation.
More concisely: For any `G` with a `DivInvMonoid` structure and any property `p` on `G`'s conjugation action, `p` is invariant under conjugation if and only if `p` holds for all elements in the image of `ConjAct G` under the `toConjAct` map.
|
ConjAct.fixedPoints_eq_center
theorem ConjAct.fixedPoints_eq_center :
∀ {G : Type u_3} [inst : Group G], MulAction.fixedPoints (ConjAct G) G = ↑(Subgroup.center G)
This theorem states that for any group `G`, the set of fixed points under the conjugation action of `G` on itself is exactly the center of `G`. In other words, an element of `G` is fixed under the conjugation action if and only if it commutes with every other element in `G`. Here, the "conjugation action" refers to the operation where an element `g` of the group acts on another element `h` by conjugation, i.e., `g * h * g⁻¹`. The "center" of a group is the set of elements that commute with all other elements, i.e., for any element `z` in the center and any element `g` in the group, `z * g = g * z`.
More concisely: The center of a group is the set of elements that are fixed under the conjugation action of the group.
|