squarefree_cyclotomic

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

English

Over any field K, the cyclotomic polynomial cyclotomic(n, K) is squarefree.

Русский

Над любым полем K циклотомиальный многочлен cyclotomic(n, K) без повторов (квадратсвободен).

LaTeX

$$Squarefree( cyclotomic_n(K) )$$

Lean4

theorem squarefree_cyclotomic (n : ℕ) (K : Type*) [Field K] [NeZero (n : K)] : Squarefree (cyclotomic n K) :=
  (separable_cyclotomic n K).squarefree

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

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

Разделы

Аффилиация

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