dvd_degree'

Mathlib.RingTheory.Polynomial.SeparableDegree

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

English

There exists m with hf.degree * q^m = f.natDegree, where hf comes from HasSeparableContraction.

Русский

Существует m, такое что hf.degree · q^m = f.natDegree, где hf происходит из HasSeparableContraction.

LaTeX

$$$\\exists m:\\mathbb{N}, hf.degree \\cdot q^m = f.natDegree$$$

Lean4

theorem dvd_degree' : ∃ m : ℕ, hf.degree * q ^ m = f.natDegree :=
  (Classical.choose_spec hf).dvd_degree'

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

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

Разделы

Аффилиация

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