eval₂_one_cyclotomic_prime_pow

Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_one_cyclotomic_prime_pow

← MathLib Explorer

English

For prime p and k, eval₂ f 1 cyclotomic(p^(k+1), R) = p.

Русский

Для простого p и k выполняется 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_pow {R S : Type*} [CommRing R] [Semiring S] (f : R →+* S) {p : ℕ} (k : ℕ)
    [Fact p.Prime] : eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = p := by simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru