A product of X^d - 1 determines the multiset of exponents

If ∏_{d ∈ D} (X^d - 1) = ∏_{e ∈ E} (X^e - 1) in ℤ[X] for multisets D, E of positive integers, then D = E. Proof: map to ℂ[X], compare the multiplicity of a primitive m-th root of unity (which counts the elements of the multiset divisible by m), then recover the multiplicities downward from the largest element.

Main results

• CyclotomicMultiset.multiset_eq_of_prod_X_pow_sub_one_eq: the statement above.

References

• C. Marín, Schur polynomials twisted by roots of unity and reciprocal pairs: exactly three factors, and where they vanish, arXiv:2608.09619 (2026), Proposition prop:minimal.

theorem CyclotomicMultiset.countP_split {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hn : p n) (D : Multiset ℕ) : Multiset.countP p D = Multiset.count n D + Multiset.countP (fun (x : ℕ) => p x ∧ ¬x = n) D

theorem CyclotomicMultiset.eq_of_countP_dvd {D E : Multiset ℕ} (hD : ∀ d ∈ D, 0 < d) (hE : ∀ e ∈ E, 0 < e) (h : ∀ (m : ℕ), 0 < m → Multiset.countP (fun (x : ℕ) => m ∣ x) D = Multiset.countP (fun (x : ℕ) => m ∣ x) E) : D = E

theorem CyclotomicMultiset.count_nthRoots (d m : ℕ) (hd : 0 < d) {ζ : ℂ} (hζ : IsPrimitiveRoot ζ m) : Multiset.count ζ (Polynomial.nthRoots d 1) = if m ∣ d then 1 else 0

theorem CyclotomicMultiset.sum_ite_eq_countP (m : ℕ) (D : Multiset ℕ) : (Multiset.map (fun (d : ℕ) => if m ∣ d then 1 else 0) D).sum = Multiset.countP (fun (x : ℕ) => m ∣ x) D

theorem CyclotomicMultiset.count_roots_prod (D : Multiset ℕ) (hD : ∀ d ∈ D, 0 < d) {m : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ m) : Multiset.count ζ (Multiset.map (fun (d : ℕ) => Polynomial.X ^ d - 1) D).prod.roots = Multiset.countP (fun (x : ℕ) => m ∣ x) D

theorem CyclotomicMultiset.multiset_eq_of_prod_X_pow_sub_one_eq {D E : Multiset ℕ} (hD : ∀ d ∈ D, 0 < d) (hE : ∀ e ∈ E, 0 < e) (h : (Multiset.map (fun (d : ℕ) => Polynomial.X ^ d - 1) D).prod = (Multiset.map (fun (e : ℕ) => Polynomial.X ^ e - 1) E).prod) : D = E