apply_fun MvPolynomial.eval fun i : Fin 2 => if i = 0 then x else y at this
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this :
  MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
⊢ 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
this :
  (MvPolynomial.eval fun i => if i = 0 then x else y) (MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n) =
    (MvPolynomial.eval fun i => if i = 0 then x else y)
      (∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1))
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)