eval_one_cyclotomic_prime — Mathlib

English

Let p be a prime and R a commutative ring. Then evaluating cyclotomic p at 1 yields p, i.e., eval(1, cyclotomic(p, R)) = p.

Русский

Пусть p — простое число. Тогда значение cyclotomic(p, R) в 1 равно p: eval(1, cyclotomic(p, R)) = p.

LaTeX

$$eval(1, cyclotomic_p(R)) = p$$

Lean4

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

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