X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd

English

If d is a proper divisor of n, then (X^d − 1) · Φ_n(R) divides X^n − 1.

Русский

Если d является правильным делителем n, то (X^d − 1) · Φ_n(R) делит X^n − 1.

LaTeX

$$$$X^d - 1 \;|\; X^n - 1 \quad\text{and}\quad (X^d - 1) \cdot \mathrm{cyclotomic} \ d\ R \;|\; X^n - 1,$$$$

Lean4

theorem X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} (h : d ∈ n.properDivisors) :
    (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1 :=
  by
  rw [Nat.mem_properDivisors] at h
  use ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
  rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot, ← Nat.insert_self_properDivisors,
    Finset.insert_sdiff_of_notMem, Finset.prod_insert, mul_assoc]
  · exact Finset.notMem_sdiff_of_notMem_left Nat.self_notMem_properDivisors
  · exact fun hk => h.2.not_ge <| Nat.divisor_le hk
  · exact h.2.ne_bot

Похожие утверждения