lift_top

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.lift_top

English

In the lattice of intermediate fields, lifting the top yields the underlying field: lift_K(⊤) = K.

Русский

В решётке промежуточных полей подъем вершины даёт исходное поле: lift_K(⊤) = K.

LaTeX

$$$\\\\operatorname{lift}_K(\\\\top) = K.$$$

Lean4

@[simp]
theorem lift_top (K : IntermediateField F E) : lift (F := K) ⊤ = K := by
  rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]

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

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

Разделы

Аффилиация

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