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.

@[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.

def «term_^+_» : Lean.TrailingParserDescr

The notation for FixedPoints.addSubgroup, chosen to resemble αᴹ.

@[simp]

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

@[simp]

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