Documentation

Mathlib.Algebra.Ring.Action.Submonoid

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 : α) :
      a addSubmonoid M α ∀ (m : M), m a = 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

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

          Equations
            Instances For
              @[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