suffices
  (X 0 : MvPolynomial (Fin 2) K) ^ (n : ℕ) - X 1 ^ (n : ℕ) =
    ∏ ζ in nthRootsFinset n K, (X 0 - MvPolynomial.C ζ * X 1)
  by
  apply_fun MvPolynomial.eval fun i : Fin 2 => if i = 0 then x else y at this
  simpa [MvPolynomial.eval_prod] using this
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)