Theorems · Theorem · group theory

SubAddAction.exists_vadd_of_last_eq

∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ}
  (a : α) (x : Fin n.succ ↪ α), ∃ g y, g +ᵥ x = SubAddAction.ofStabilizer.snoc y

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddAction.IsPretransitive