simpa [homogenization_prod, Polynomial.algebraMap_eq, hpos]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝¹ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this✝ :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
this :
  homogenization 1 (MvPolynomial.X 0 ^ n - 1) =
    homogenization 1 (∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
no goals