The subgroup of fixed points of an action #
def
FixedPoints.addSubmonoid
(M : Type u_1)
(α : Type u_2)
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
:
The additive submonoid of elements fixed under the whole action.
Equations
Instances For
@[simp]
theorem
FixedPoints.mem_addSubmonoid
(M : Type u_1)
(α : Type u_2)
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
(a : α)
:
def
FixedPoints.addSubgroup
(M : Type u_1)
(α : Type u_2)
[Monoid M]
[AddGroup α]
[DistribMulAction M α]
:
The additive subgroup of elements fixed under the whole action.
Equations
Instances For
@[simp]
theorem
FixedPoints.addSubgroup_toAddSubmonoid
(M : Type u_1)
(α : Type u_2)
[Monoid M]
[AddGroup α]
[DistribMulAction M α]
: