lift_bot

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

In the lattice of intermediate fields, lifting bottom element yields bottom: lift_K(⊥) = ⊥.

Русский

В решётке промежуточных полей подъём нуля даёт ноль: lift_K(⊥) = ⊥.

LaTeX

$$$\\\\operatorname{lift}_K(\\\\bot) = \\\\bot.$$$

Lean4

@[simp]
theorem lift_bot (K : IntermediateField F E) : lift (F := K) ⊥ = ⊥ :=
  map_bot _

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

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

Разделы

Аффилиация

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