coe_gen

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

For α ∈ E, F⟮α⟯ ≤ K if and only if α ∈ K, where K is an intermediate field over F.

Русский

Для α ∈ E верно F⟮α⟯ ≤ K тогда и только тогда, когда α ∈ K.

LaTeX

$$$\\\\operatorname{adjoin}_{F}(\\\\{\\\\alpha\\\\}) \\\\le K \\\\iff \\\\alpha \\\in K.$$$

Lean4

@[simp]
theorem coe_gen : (AdjoinSimple.gen F α : E) = α :=
  rfl

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

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

Разделы

Аффилиация

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