isSplittingField_C

Mathlib.FieldTheory.SplittingField.IsSplittingField

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

English

For every a in K, the constant polynomial C a is split over K with splitting field K.

Русский

Для любого a ∈ K константный полином C a распадается над K, и поле развилки равно K.

LaTeX

$$$\\forall a \\in K, \\ \\mathrm{IsSplittingField}(K,K,\\mathrm{C}(a))$$$

Lean4

theorem isSplittingField_C (a : K) : Polynomial.IsSplittingField K K (C a)
    where
  splits' := by simp
  adjoin_rootSet' := by simp

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

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

Разделы

Аффилиация

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