English
If m | n and m ≠ n with n > 0, then X^m − 1 divides the product ∏_{i ∈ Nat.properDivisors n} Φ_i(R).
Русский
Если m делит n и m ≠ n при n>0, то X^m − 1 делит произведение ∏_{i ∈ Nat.properDivisors n} Φ_i(R).
LaTeX
$$$$0 < n \Rightarrow m \mid n \land m \neq n \Rightarrow X^m - 1 \mid \prod_{i \in \mathrm{Nat.properDivisors}\ n} \mathrm{cyclotomic}\ i\ R.$$$$
Lean4
/-- If `m` is a proper divisor of `n`, then `X ^ m - 1` divides
`∏ i ∈ Nat.properDivisors n, cyclotomic i R`. -/
theorem X_pow_sub_one_dvd_prod_cyclotomic (R : Type*) [CommRing R] {n m : ℕ} (hpos : 0 < n) (hm : m ∣ n)
(hdiff : m ≠ n) : X ^ m - 1 ∣ ∏ i ∈ Nat.properDivisors n, cyclotomic i R :=
by
replace hm := Nat.mem_properDivisors.2 ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩
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)]
exact ⟨∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩
