Elliptic curves with same j-invariants are isomorphic

Main results

• WeierstrassCurve.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 WeierstrassCurve.exists_variableChange_of_j_eq {F : Type u_1} [Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [E.IsElliptic] [E'.IsElliptic] (heq : E.j = E'.j) : ∃ (C : 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.