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.

Estimated changes

added theorem EllipticCurve.map_j