Commit 2026-02-13 16:28 709c07e8
View on Github →feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective (#33403)
Let G be a finite commutative group and let H be a subgroup. If M is a commutative monoid
such that G →* Mˣ and H →* Mˣ are both finite (this is the case for example if M is a
commutative domain), then any homomorphism H →* Mˣ can be extended to an homomorphism G →* Mˣ.