algebraMap_gen

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

The canonical map from F⟮α⟯ to E sends the generator AdjoinSimple.gen F α to α.

Русский

каноническое отображение F⟮α⟯ → E отправляет генератор AdjoinSimple.gen F α в α.

LaTeX

$$$\operatorname{algebraMap} F⟮α⟯ E (AdjoinSimple.gen F α) = α$$$

Lean4

theorem algebraMap_gen : algebraMap F⟮α⟯ E (AdjoinSimple.gen F α) = α :=
  rfl

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

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

Разделы

Аффилиация

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