Commit 2024-02-23 22:00 4d0e6387

feat(AlgebraicGeometry/EllipticCurve/Projective): implement equations and nonsingularity for projective coordinates (#9416) Define a projective point representative over a ring R as the type Fin 3 -> R, and its equivalence class PointClass as a quotient by the usual scaling relation. Define the analogous equation and nonsingular predicates on Fin 3 -> F over a field F, and lift nonsingular to PointClass. This also has minimal API (e.g. it's missing many of the equation lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #8485