mathlib

a7415855 - chore(algebra/group): make `coe_norm_subgroup` and `submodule.norm_coe` consistent (#11427)

chore(algebra/group): make `coe_norm_subgroup` and `submodule.norm_coe` consistent (#11427) The `simp` lemmas for norms in a subgroup and in a submodule disagreed: the first inserted a coercion to the larger group, the second deleted the coercion. Currently this is not a big deal, but it will become a real issue when defining `add_subgroup_class`. I want to make them consistent by pointing them in the same direction. The consensus in the [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Simp.20normal.20form.3A.20coe_norm_subgroup.2C.20submodule.2Enorm_coe) suggests `simp` should insert a coercion here, so I went with that. After making the changes, a few places need extra `simp [submodule.coe_norm]` on the local hypotheses, but nothing major.