Commit 2025-10-11 18:15 831fa5ab

chore: generalise extensionality lemmas for localization (#30173) This PR generalises some extensionality lemmas for morphisms from localization. The codomains are generalised from CommMonoid to Monoid, and from CommSemiring to Semiring. Then two new extensionality lemmas for algebra morphisms are added. Currently Submonoid.LocalizationMap.epic_of_localizationMap says that if M and P are commutative monoids, and f : M →* N is a localization map for a submonoid S, then two monoid homs j k : N →* P are equal if they are equal after composing with f. This PR relaxes the assumption on P from CommMonoid to Monoid. Similar generalisations are made in other places, and then two new lemmas for AlgHom are added.