The subgroup of fixed points of an action

def FixedPoints.addSubmonoid (M : Type u_1) (α : Type u_2) [Monoid M] [AddMonoid α] [DistribMulAction M α] : AddSubmonoid α

The additive submonoid of elements fixed under the whole action.

Equations

• FixedPoints.addSubmonoid M α = { carrier := MulAction.fixedPoints M α, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem FixedPoints.mem_addSubmonoid (M : Type u_1) (α : Type u_2) [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : α) : a ∈ addSubmonoid M α ↔ ∀ (m : M), m • a = a

def FixedPoints.addSubgroup (M : Type u_1) (α : Type u_2) [Monoid M] [AddGroup α] [DistribMulAction M α] : AddSubgroup α

The additive subgroup of elements fixed under the whole action.

Equations

• FixedPoints.addSubgroup M α = { toAddSubmonoid := FixedPoints.addSubmonoid M α, neg_mem' := ⋯ }

@[simp]

theorem FixedPoints.mem_addSubgroup (M : Type u_1) (α : Type u_2) [Monoid M] [AddGroup α] [DistribMulAction M α] (a : α) : a ∈ addSubgroup M α ↔ ∀ (m : M), m • a = a

@[simp]

theorem FixedPoints.addSubgroup_toAddSubmonoid (M : Type u_1) (α : Type u_2) [Monoid M] [AddGroup α] [DistribMulAction M α] : (addSubgroup M α).toAddSubmonoid = addSubmonoid M α