def JInvariant.shortWeierstrassCurve {k : Type u_1} [Field k] (A B : k) : WeierstrassCurve k

The short Weierstrass curve $y^2 = x^3 + Ax + B$ given by setting $a_1 = a_2 = a_3 = 0$, $a_4 = A$, $a_6 = B$.

def JInvariant.jInvariant {k : Type u_1} [Field k] (A B : k) : k

Definition 13.11. The $j$-invariant of the short Weierstrass curve $y^2 = x^3 + Ax + B$: $j(A, B) = 1728 \cdot 4A^3 / (4A^3 + 27B^2)$.

@[simp]

theorem JInvariant.shortWeierstrassCurve_c₄ {k : Type u_1} [Field k] (A B : k) : (shortWeierstrassCurve A B).c₄ = -48 * A

The $c_4$ invariant of the short Weierstrass curve $y^2 = x^3 + Ax + B$ equals $-48 A$.

@[simp]

theorem JInvariant.shortWeierstrassCurve_Δ {k : Type u_1} [Field k] (A B : k) : (shortWeierstrassCurve A B).Δ = -16 * (4 * A ^ 3 + 27 * B ^ 2)

The discriminant of the short Weierstrass curve $y^2 = x^3 + Ax + B$ equals $-16(4A^3 + 27B^2)$.

theorem JInvariant.sixteen_ne_zero_of_two_ne_zero {k : Type u_1} [Field k] (h2 : 2 ≠ 0) : 16 ≠ 0

If $2 \ne 0$ in $k$, then $16 \ne 0$ in $k$.

theorem JInvariant.shortWeierstrassCurve_isElliptic {k : Type u_1} [Field k] (A B : k) (h2 : 2 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) : (shortWeierstrassCurve A B).IsElliptic

A short Weierstrass curve $y^2 = x^3 + Ax + B$ is elliptic provided $2 \ne 0$ in $k$ and $4A^3 + 27B^2 \ne 0$.

theorem JInvariant.j_eq_jInvariant {k : Type u_1} [Field k] (A B : k) (h2 : 2 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) : (shortWeierstrassCurve A B).j = jInvariant A B

Mathlib's $j$-invariant of the short Weierstrass curve agrees with the textbook formula $1728 \cdot 4A^3 / (4A^3 + 27B^2)$.

@[simp]

theorem JInvariant.jInvariant_of_A_eq_zero {k : Type u_1} [Field k] (B : k) : jInvariant 0 B = 0

When $A = 0$, the curve $y^2 = x^3 + B$ has $j$-invariant $0$.

theorem JInvariant.jInvariant_of_B_eq_zero {k : Type u_1} [Field k] (A : k) (hA : A ≠ 0) (h2 : 2 ≠ 0) : jInvariant A 0 = 1728

When $B = 0$ and $A \ne 0$, the curve $y^2 = x^3 + Ax$ has $j$-invariant $1728$.