Commit 2024-10-16 04:43 52ec24b8

feat(AlgebraicGeometry/EllipticCurve/J): further properties of j-invariants of elliptic curves (#17431) Currently there is only one new result:

• EllipticCurve.exists_variableChange_of_j_eq: if E and E' are elliptic curves with the same j-invariants defined over a separably closed field, then there exists a change of variables over that field which change E into E'. For convenience, a few new results for normal forms are added to EllipticCurve namespace, parallel to that of WeierstrassCurve. Also added some convenience auxiliary results used in this PR:
• Algebra/CharP/Defs: CharP.cast_ne_zero_of_ne_of_prime
• FieldTheory/Separable: Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C[']
• FieldTheory/IsSepClosed: IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C[']