lift

Mathlib.FieldTheory.SplittingField.Construction

URI: https://scilib.ai/kg/mathlib#Polynomial.SplittingField.lift

← MathLib Explorer

English

Any splitting field of f over K is isomorphic to SplittingField f.

Русский

Любое развёртывающее поле f над K изоморфно SplittingField f.

LaTeX

$$$L \cong_K \mathrm{SplittingField}(f)$ for any IsSplittingField K L f$$

Lean4

/-- Embeds the splitting field into any other field that splits the polynomial. -/
def lift : SplittingField f →ₐ[K] L :=
  IsSplittingField.lift f.SplittingField f hb

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

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

Разделы

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

Аффилиация

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