eval_one_cyclotomic_prime_pow — Mathlib

English

For prime p and k, eval 1 cyclotomic(p^(k+1), R) equals p (in the appropriate target).

Русский

Для простого числа p и целого k выражение eval 1 cyclotomic(p^(k+1), R) равно p.

LaTeX

$$eval(1, cyclotomic(p^(k+1), R)) = p$$

Lean4

@[simp]
theorem eval_one_cyclotomic_prime_pow {R : Type*} [CommRing R] {p : ℕ} (k : ℕ) [hn : Fact p.Prime] :
    eval 1 (cyclotomic (p ^ (k + 1)) R) = p := by
  simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, eval_X, one_pow, Finset.sum_const, eval_pow, eval_finset_sum,
    Finset.card_range, smul_one_eq_cast]

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