Zulip Chat Archive

Stream: maths

Topic: add_comm_subgroup


view this post on Zulip Patrick Massot (Apr 08 2019 at 14:25):

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


Last updated: May 14 2021 at 20:13 UTC