coe_inclusion

Mathlib.FieldTheory.IntermediateField.Basic

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

English

For hEF: E ≤ F and e ∈ E, the map inclusion hEF sends e to the same element in L.

Русский

Для hEF: E ≤ F и e ∈ E отображение включения отправляет e в то же значение в L.

LaTeX

$$$ (inclusion hEF e) = e $$$

Lean4

@[simp]
theorem coe_inclusion {E F : IntermediateField K L} (hEF : E ≤ F) (e : E) : (inclusion hEF e : L) = e :=
  rfl

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

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

Разделы

Аффилиация

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