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

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

def «term_^+_» : Lean.TrailingParserDescr

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

Equations

• «term_^+_» = Lean.ParserDescr.trailingNode `«term_^+_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^+") (Lean.ParserDescr.cat `term 51))

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