cyclotomic_prime_pow_mul_X_pow_sub_one

English

If p is prime, then Φ_{p^{n+1}}(R) equals the sum ∑_{i=0}^{p-1} (X^{p^n})^i.

Русский

Если p — простое, Φ_{p^{n+1}}(R) = ∑_{i=0}^{p-1} (X^{p^n})^i.

LaTeX

$$$$\mathrm{cyclotomic}\ (p^{(n+1)})\ R = \sum_{i=0}^{p-1} (X^{p^n})^{i}.$$$$

Lean4

theorem cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type*) [CommRing R] (p k : ℕ) [hn : Fact (Nat.Prime p)] :
    cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1 := by
  rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]

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