K✝ : Type ?u.240784
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : Set.PairwiseDisjoint ↑(Nat.divisors n) fun k => primitiveRoots k K
⊢ ∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1
K✝ : Type ?u.240784
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1
have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K :=
  fun x _ y _ hne => IsPrimitiveRoot.disjoint hne
no goals
K✝ : Type ?u.240784
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : Set.PairwiseDisjoint ↑(Nat.divisors n) fun k => primitiveRoots k K
⊢ ∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
  h.nthRoots_one_eq_biUnion_primitiveRoots]