# 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 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.