natSepDegree_X_pow

Mathlib.FieldTheory.SeparableDegree

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

English

The separable degree of X^n is 0 if n = 0, and 1 otherwise.

Русский

Разделяемая степень X^n равна 0 при n=0 и 1 при n>0.

LaTeX

$$$ (X^n).\operatorname{natSepDegree} = \begin{cases} 0, & n=0 \\\ 1, & n\neq 0 \end{cases}$$$

Lean4

theorem natSepDegree_X_pow {n : ℕ} : (X ^ n : F[X]).natSepDegree = if n = 0 then 0 else 1 := by
  simp only [natSepDegree_pow, natSepDegree_X]

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

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

Разделы

Аффилиация

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