algebraMap_gen₂

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.AdjoinPair.algebraMap_gen₂

English

Under the natural algebra map to L, the image of gen₂ is y.

Русский

При естественном отображении алгебраMap в L образ gen₂ равен y.

LaTeX

$$ (\operatorname{algebraMap} (K⟮x,y⟯ \to L))(\mathrm{gen}_2) = y $$

Lean4

theorem algebraMap_gen₂ : (algebraMap (↥K⟮x, y⟯) L) (gen₂ K x y) = y :=
  rfl

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

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

Разделы

Аффилиация

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