diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
index 8575fbac2391b0..56ac335aa2b4f4 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@@ -395,6 +395,10 @@ lemma j_eq_zero (h : W.c₄ = 0) : W.j = 0 := by
 lemma j_eq_zero_iff [IsReduced R] : W.j = 0 ↔ W.c₄ = 0 := by
   rw [j_eq_zero_iff', pow_eq_zero_iff three_ne_zero]
 
+theorem j_eq {K : Type*} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] :
+    W.j = W.Δ⁻¹ * W.c₄ ^ 3 := by
+  rw [WeierstrassCurve.j, Units.val_inv_eq_inv_val, WeierstrassCurve.coe_Δ']
+
 section CharTwo
 
 variable [CharP R 2]