Commit 2023-08-03 09:17 06ace73a

feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant (#5935) Main changes:

• Define specific Weierstrass curves, whose j-invariants should be 0, 1728, or ≠ 0 and 1728.
• Prove the quantities c₄, Δ and j for them (whenever they are defined).
• Define an elliptic curve from an element j in a field, whose j-invariant is equal to j.
• Generalize Inhabited (EllipticCurve ℚ) to Inhabited (EllipticCurve F) for any field F (computable if F has DecidableEq).