Commit 2024-08-07 11:50 aeb3c058

View on Github →

feat(Subgroup/IsCommutative): add instance for MonoidHom.range (#15370) This PR adds:

  • instance Subgroup.commGroup_isCommutative [CommGroup G] (H : Subgroup G) : H.IsCommutative for subgroups of an abelian group; and
  • instance MonoidHom.range_isCommutative [CommGroup G] (f : G →* N) : f.range.IsCommutative, for the range of a MonoidHom whose domain is abelian. It also adds a lemma Subgroup.mul_comm_of_mem_isCommutative to allow applying the commutativity without constructing terms of a Subgroup. (This lemma is included in this same PR as I mentioned it in the same Zulip thread, but is independent of the two instances above.) Please refer to the Zulip thread for discussions.

Estimated changes