algebraMap_mem

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.adjoin.algebraMap_mem

English

The image of the base field under algebraMap F E lies in adjoin F S.

Русский

Образ алгебраMap F E содержится в adjoin F S.

LaTeX

$$$\text{algebraMap}_{F,E}(x) \in \operatorname{adjoin}_F S \quad \text{for all } x \in F$$$

Lean4

theorem algebraMap_mem (x : F) : algebraMap F E x ∈ adjoin F S :=
  IntermediateField.algebraMap_mem (adjoin F S) x

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

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

Разделы

Аффилиация

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