MulAction.fixedBy_inv
theorem MulAction.fixedBy_inv :
∀ (α : Type u_1) {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G),
MulAction.fixedBy α g⁻¹ = MulAction.fixedBy α g
This theorem states that in a multiplicative group action, the set of points which are left unchanged by the action of the element `g` is the same as the set of points left unchanged by the action of the inverse of `g`, denoted `g⁻¹`. Here, `MulAction.fixedBy α g` represents the set of all points in the space `α` fixed by the group element `g`. So the theorem essentially says that if a point doesn't move under the action of a group element, it also won't move under the action of the inverse of that group element.
More concisely: In a multiplicative group action, the sets of fixed points for an element and its inverse are equal.
|
Mathlib.GroupTheory.GroupAction.FixedPoints._auxLemma.2
theorem Mathlib.GroupTheory.GroupAction.FixedPoints._auxLemma.2 :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {m : M} {a : α},
(a ∈ MulAction.fixedBy α m) = (m • a = a)
This theorem states that for any monoid `M` and any type `α` that has a `MulAction` from `M`, an element `a` of type `α` is in the set of elements fixed by a monoidal element `m` if and only if the action of `m` on `a` leaves `a` unchanged. In other words, `a` is fixed by `m` precisely when `m` acting on `a` equals `a`.
More concisely: For any monoid `M` and type `α` with an `MulAction` from `M`, an element `a` of type `α` is fixed by a monoidal element `m` if and only if `m * a = a`.
|
AddAction.fixedBy_neg
theorem AddAction.fixedBy_neg :
∀ (α : Type u_1) {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G),
AddAction.fixedBy α (-g) = AddAction.fixedBy α g
The theorem `AddAction.fixedBy_neg` states that for any additive group action, the set of points fixed by an element `g` from the additive group `G` is the same as the set of points fixed by the additive inverse of `g` (denoted as `-g`). In other words, if an element `x` from the set `α` remains unchanged under the action of `g`, it will also remain unchanged under the action of `-g`. This is a property of group actions in the context of group theory.
More concisely: For any additive group action, the set of points fixed by an element is equal to the set of points fixed by its additive inverse.
|
Mathlib.GroupTheory.GroupAction.FixedPoints._auxAddLemma.2
theorem Mathlib.GroupTheory.GroupAction.FixedPoints._auxAddLemma.2 :
∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {m : M} {a : α},
(a ∈ AddAction.fixedBy α m) = (m +ᵥ a = a)
The theorem `Mathlib.GroupTheory.GroupAction.FixedPoints._auxAddLemma.2` states that for any type `M` with an additive monoid structure, any type `α` with an `M`-additive action, any element `m` of `M`, and any element `a` of `α`, `a` is in the set of elements fixed by `m` (i.e., `a` is in `AddAction.fixedBy α m`) if and only if `m` added to `a` via the additive action (`m +ᵥ a`) equals `a` itself. In essence, the theorem formalizes the definition of fixed points under an additive action of a monoid.
More concisely: For any additive monoid M, type α with an M-additive action, element m of M, and α-element a, a is a fixed point of the action by m if and only if m + a = a.
|