Further properties of j-invariants of elliptic curves

This file states some further properties of j-invariants of elliptic curves.

Main results

• 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'.

theorem EllipticCurve.exists_variableChange_of_j_eq {F : Type u_1} [Field F] [IsSepClosed F] (E : EllipticCurve F) (E' : EllipticCurve F) (heq : E.j = E'.j) : ∃ (C : WeierstrassCurve.VariableChange F), E.variableChange C = E'

If there are two 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 one curve into another.