separable_cyclotomic — Mathlib

English

For any field K and natural n with n ≠ 0 in K, the cyclotomic polynomial cyclotomic(n, K) is separable over K.

Русский

Для поля K и натурального n с n ≠ 0 в K многочлен циклотомициклический cyclotomic(n, K) разлагaем над K без повторов.

LaTeX

$$Separable( cyclotomic_n(K) )$$

Lean4

theorem separable_cyclotomic (n : ℕ) (K : Type*) [Field K] [NeZero (n : K)] : (cyclotomic n K).Separable :=
  .of_dvd (separable_X_pow_sub_C 1 NeZero.out one_ne_zero) (cyclotomic.dvd_X_pow_sub_one n K)

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