Theorems · Definition · group theory

SubMulAction.ofStabilizer.snoc

{G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] → {a : α} → {n : ℕ} → (Fin n ↪ ↥(SubMulAction.ofStabilizer G a)) → Fin n.succ ↪ α

Append a to x : Fin n ↪ ofStabilizer G a to get an element of Fin n.succ ↪ α.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Cited by

4 results in Mathlib

Foundations

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

Assumes

GroupMulAction