∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R},
  W'.polynomialY =
    MvPolynomial.C 2 * MvPolynomial.X 1 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 +
      MvPolynomial.C W'.a₃ * MvPolynomial.X 2 ^ 3