Commit 2024-02-19 17:38 83de2454
View on Github →refactor(AlgebraicGeometry/EllipticCurve/*): rename baseChange to map (#9744)
This is in accordance with other similar definitions e.g. Polynomial.map
. It turns out that rewrite lemmas of the form (W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)
are rather annoying to use, so they are replaced with the original baseChange
functionality that says (W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)
. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve W
rather than its points.