mathlib3

be87e250 - feat(topology/algebra): subgroup.is_closed_of_discrete (#16130)