Commit 2024-06-17 16:07 b9b6c25c
View on Github →feat(EllipticCurve): a coordinate ring over a domain is a domain (#12883)
Generalize instIsDomainCoordinateRing from normalized GCD domains to all domains, by reducing to the field case via the injective ring hom to the field of fractions. (This works basically because the coordinate ring is a free module over the base ring and therefore flat.) To get this done, we move various declarations (some instances and basis API) up, and introduce CoordinateRing.map/map_mk/map_smul/map_injective.