Commit 2022-02-04 21:12 a7415855

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 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.