eval₂_one_cyclotomic_prime — Mathlib

English

For a prime p and natural k, and a Ring hom f, the evaluation of cyclotomic(p^(k+1), R) at 1 via f yields p: eval₂ f 1 cyclotomic(p^(k+1), R) = p.

Русский

Для простого p и целого k, через отображение f верна формула eval₂ f 1 cyclotomic(p^(k+1), R) = p.

LaTeX

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

Lean4

theorem eval₂_one_cyclotomic_prime {R S : Type*} [CommRing R] [Semiring S] (f : R →+* S) {p : ℕ} [Fact p.Prime] :
    eval₂ f 1 (cyclotomic p R) = p := by simp

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