Theorems · Definition · group theory

SubAddAction.ofFixingAddSubgroup_of_singleton

(M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          have φ := fun x =>
            match x with
            | ⟨m, hm⟩ => ⟨m, ⋯⟩;
          ↥(SubAddAction.ofFixingAddSubgroup M {a}) →ₑ[φ] ↥(SubAddAction.ofStabilizer M a)

The equivariant map between SubAddAction.ofStabilizer M a and ofFixingAddSubgroup M {a}.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction