add_comm_subgroup

Stream: maths

[Patrick Massot]

Is it me or mathlib is missing:

instance add_comm_subgroup {α : Type*} [add_comm_group α] (s : set α) [is_add_subgroup s] : add_comm_group s :=
by subtype_instance

I get the add_group s without any problem but not commutativity