separable_X

Mathlib.FieldTheory.Separable

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

English

The polynomial X is separable over any commutative semiring.

Русский

Многочлен X разделим над любым коммутативным полукольцом.

LaTeX

$$$\\operatorname{Separable}(X)$$$

Lean4

theorem separable_X : (X : R[X]).Separable :=
  by
  rw [separable_def, derivative_X]
  exact isCoprime_one_right

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

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

Разделы

Аффилиация

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