R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hm : m ∣ n
hdiff : m ≠ n
⊢ X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R
replace hm := Nat.mem_properDivisors.2
  ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ (∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R) * (X ^ m - 1)
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R
rw [← Finset.sdiff_union_of_subset (Nat.divisors_subset_properDivisors (ne_of_lt hpos).symm
  (Nat.mem_properDivisors.1 hm).1 (ne_of_lt (Nat.mem_properDivisors.1 hm).2)),
  Finset.prod_union Finset.sdiff_disjoint,
  prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)]
no goals
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ (∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R) * (X ^ m - 1)
exact ⟨∏ x : ℕ in n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩
no goals
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ (∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R) * (X ^ m - 1) =
    (X ^ m - 1) * ∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R
rw [mul_comm]