dvd_degree

Mathlib.RingTheory.Polynomial.SeparableDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.HasSeparableContraction.dvd_degree

← MathLib Explorer

English

The separable degree hf.degree divides the (absolute) degree f.natDegree.

Русский

Разделимая степень hf.degree делит полное вырожденное число f.natDegree.

LaTeX

$$$hf.degree \\mid f.natDegree$$$

Lean4

/-- The separable degree divides the degree. -/
theorem dvd_degree : hf.degree ∣ f.natDegree :=
  let ⟨a, ha⟩ := hf.dvd_degree'
  Dvd.intro (q ^ a) ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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