cyclotomic_one — Mathlib

English

The first cyclotomic polynomial is X - 1.

Русский

Первый циклотоми́ческий полином равен X - 1.

LaTeX

$$$\operatorname{cyclotomic}(1,R) = X - 1$$$

Lean4

/-- The first cyclotomic polynomial is `X - 1`. -/
@[simp]
theorem cyclotomic_one (R : Type*) [Ring R] : cyclotomic 1 R = X - 1 :=
  by
  have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
    simp only [cyclotomic'_one, map_X, Polynomial.map_one, Polynomial.map_sub]
  symm
  rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]
  simp only [map_X, Polynomial.map_one, Polynomial.map_sub]

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