primitive_element_root

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.primitive_element_root

← MathLib Explorer

English

If h : IsAdjoinRoot E f, then the subfield generated by h.root over F is the whole field E; i.e., F⟮h.root⟯ = ⊤.

Русский

Если h : IsAdjoinRoot E f, то поле, порождаемое корнем h.root над F, равно всему полю E.

LaTeX

$$F⟮h.root⟯ = ⊤$$

Lean4

theorem primitive_element_root (h : IsAdjoinRoot E f) : F⟮h.root⟯ = ⊤ :=
  IntermediateField.adjoin_eq_top_of_algebra F { h.root } (adjoin_root_eq_top h)

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

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

Разделы

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

Аффилиация

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