is_group_hom.range_subgroup

Stream: general

[Kenny Lau]

instance is_group_hom.range_subgroup : is_subgroup (set.range f) :=
@set.image_univ _ _ f ▸ is_group_hom.image_subgroup f set.univ

Could you add this to mathlib? @Mario Carneiro