case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : AddGroup α
inst✝ : AddAction α β
g : α
x : β
h : α
⊢ h ∈ stabilizer α (g +ᵥ x) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer α x)
α : Type u
β : Type v
γ : Type w
inst✝¹ : AddGroup α
inst✝ : AddAction α β
g : α
x : β
⊢ stabilizer α (g +ᵥ x) = AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer α x)
ext h
no goals
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : AddGroup α
inst✝ : AddAction α β
g : α
x : β
h : α
⊢ h ∈ stabilizer α (g +ᵥ x) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer α x)
rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
  add_left_neg, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
  AddAut.conj_symm_apply]