∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R},
  W'.polynomialX =
    MvPolynomial.C W'.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 -
      (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 +
        MvPolynomial.C W'.a₄ * MvPolynomial.X 2 ^ 2)