X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd

English

For any R, and integers d, n with d | n and n ≠ 0, the equality (X^d − 1) · ∏_{x ∈ n.divisors \ d.divisors} Φ_x(R) = X^n − 1 holds.

Русский

Для любого R и таких d, n, что d | n и n ≠ 0, выполняется равенство (X^d − 1) · ∏_{x ∈ n.divisors \ d.divisors} Φ_x(R) = X^n − 1.

LaTeX

$$$$0 < d ⇒ (X^d - 1) \cdot \bigg(\prod_{x \in n.divisors \ d.divisors} \mathrm{cyclotomic}\ x\ R\bigg) = X^n - 1.$$$$

Lean4

theorem X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ} (hdvd : d ∣ n)
    (hn : n ≠ 0) : ((X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) = X ^ n - 1 :=
  by
  have h0d : 0 < d := Nat.pos_of_dvd_of_pos hdvd (by positivity)
  rw [← prod_cyclotomic_eq_X_pow_sub_one h0d, ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]

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