Commit 2026-03-06 17:10 a3d25298

feat(AlgebraicGeometry/EllipticCurve/Affine/Point): expose coordinates (#36270) This PR seems to add a lot of noise, but there are two good reasons for it:

• Currently the infoview shows Point.some ... for any affine point, so the computation of an addition of two points would show Point.some ... + Point.some ... = Point.some ... in the infoview, so the user has to hover over each of them to see what's going on.
• When creating (resp extracting) the coordinates of explicit points in downstream files, one needs to type Point.some (x := x) (y := y) h (resp @Point.some _ _ _ x y h) to create (resp extract) an affine point (x, y) and the proof h that it is nonsingular, which has been pretty annoying so far. Of course the former can be solved by some metaprogramming / pretty printing, but I think the latter is good enough a reason to have this quality of life change.