adjoin_rootSet_eq_range

Mathlib.FieldTheory.SplittingField.IsSplittingField

URI: https://scilib.ai/kg/mathlib#Polynomial.IsSplittingField.adjoin_rootSet_eq_range

← MathLib Explorer

English

For f ∈ K[X], if [IsSplittingField K L f], then f splits over L.

Русский

Если f имеет IsSplittingField над K в L, то f распадается над L.

LaTeX

$$splits (IsSplittingField)$$

Lean4

theorem adjoin_rootSet_eq_range [Algebra K F] (f : K[X]) [IsSplittingField K L f] (i : L →ₐ[K] F) :
    Algebra.adjoin K (rootSet f F) = i.range :=
  (Polynomial.adjoin_rootSet_eq_range (splits L f) i).mpr (adjoin_rootSet L f)

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

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

Разделы

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

Аффилиация

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