cyclotomic_prime_mul_X_sub_one

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.cyclotomic_prime_mul_X_sub_one

← MathLib Explorer

English

For a prime p, Φ_p(R) · (X − 1) = X^p − 1.

Русский

Для простого p выполняется Φ_p(R) · (X − 1) = X^p − 1.

LaTeX

$$$$\mathrm{cyclotomic}\ p\ R \cdot (X - 1) = X^p - 1.$$$$

Lean4

theorem cyclotomic_prime_mul_X_sub_one (R : Type*) [Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)] :
    cyclotomic p R * (X - 1) = X ^ p - 1 := by rw [cyclotomic_prime, geom_sum_mul]

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

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

Разделы

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

Аффилиация

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