# The subgroup of fixed points of an action #

source
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' := ⋯ }

Instances For

source
@[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
source
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' := ⋯ }

Instances For

source
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))

Instances For

source
@[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
source
@[simp]
theorem FixedPoints.addSubgroup_toAddSubmonoid (M : Type u_1) (α : Type u_2) [Monoid M] [AddGroup α] [DistribMulAction M α] :
(α^+M).toAddSubmonoid = addSubmonoid M α