separable_minpoly

Mathlib.FieldTheory.Minpoly.ConjRootClass

URI: https://scilib.ai/kg/mathlib#ConjRootClass.separable_minpoly

English

If K ⊆ L is separable (Algebra.IsSeparable K L), then c.minpoly is Separable.

Русский

Если расширение K ⊆ L разбираемо (разделимо), то c.minpoly распадается на простые корни отдельно.

LaTeX

$$$ c.minpoly \\text{ Separable}$$$

Lean4

theorem separable_minpoly (c : ConjRootClass K L) : Separable c.minpoly :=
  by
  induction c
  exact Algebra.IsSeparable.isSeparable K _

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

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

Разделы

Аффилиация

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