Commit 2024-11-29 22:48 cee87aa2

refactor(AlgebraicGeometry/EllipticCurve/*): add WeierstrassCurve.IsElliptic and remove EllipticCurve (#18531) The original EllipticCurve is WeierstrassCurve bundled with Δ' : Rˣ and a proof that Δ' = Δ. This definition makes Δ' and j computable, but at the expense that some APIs must be duplicated for EllipticCurve and WeierstrassCurve. This PR adds the typeclass WeierstrassCurve.IsElliptic which asserts that IsUnit W.Δ, and which is a Prop. The old API for elliptic curves are replaced by a WeierstrassCurve W together with [W.IsElliptic]. The caveat is that Δ' and j becomes noncomputable. The original design of this PR is WeierstrassCurve.Elliptic which is Invertible W.Δ, and which is a Type. By this design Δ' and j remain computable. But this design makes simpNF linter timeout. So this design is abandoned and replaced by current design. Also rename J.lean -> IsomOfJ.lean and split ModelsWithJ.lean.