Commit 2024-01-10 15:56 1c6c79f0

refactor(AlgebraicGeometry/EllipticCurve/*): refactor base change for ring homomorphisms (#9596) Refactor Weierstrass curves and nonsingular rational points to allow for base changes over an arbitrary ring homomorphism φ : K →+* L. This generalises the natural map algebraMap K L and removes the necessity for Algebra K L, but also gives an easy way to define DistribMulAction for the action of L ≃ₐ[K] L on the nonsingular rational points over L, since L ≃ₐ[K] L restricts to L →ₐ[K] L that restricts to L →+* L. The old notation W⟮L⟯ is preserved for base change over algebraMap K L. Also remove some unnecessary coercions in the Weierstrass file.