pointwise conj_act on normal subgroups

Stream: Is there code for X?

[Chris Birkbeck]

Do we have:

lemma conj_act_normal {G : Type*} [group G] (H : subgroup G) (hH : H.normal ) (g : conj_act G) :
  g • H = H :=
begin
sorry,
end

It feels like the sort of thing we should have somewhere but I can't find it.

[Eric Wieser]

I don't think we have that, as conj_act and pointwise actions are fairly recent

[Eric Wieser]

@Chris Hughes would likely have added it if we did have it

[Chris Hughes]

I don't remember if I added it