Theorems · Theorem · group theory

AddAction.le_stabilizer_vadd_left

∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddAction G β]
  [inst_3 : VAdd α β] [VAddAssocClass G α β] (a : α) (b : β), AddAction.stabilizer G a ≤ AddAction.stabilizer G (a +ᵥ b)

Defined in

Mathlib.GroupTheory.GroupAction.Defs

Cited by

1 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddActionAddActionVAddVAddAssocClass