Commit 2023-01-23 22:33 808ea4eb

feat(algebraic_geometry/elliptic_curve/weierstrass): define a basis for the coordinate ring (#18101) Also refactor coordinate_ring definitions and lemmas into the coordinate_ring namespace, and compute the degree of the norm of an element of the coordinate_ring as an R[X]-algebra in terms of this basis.