comap_top

Mathlib.Algebra.Field.Subfield.Basic

URI: https://scilib.ai/kg/mathlib#Subfield.comap_top

English

Let f: K →+* L. The preimage under f of the top subfield is the top subfield: (⊤).comap f = ⊤.

Русский

Пусть f: K →+* L. Предобраз верха подполе от f равен верху: (⊤).comap f = ⊤.

LaTeX

$$$$(\top : Subfield L).comap f = \top$$$$

Lean4

@[simp]
theorem comap_top (f : K →+* L) : (⊤ : Subfield L).comap f = ⊤ :=
  (gc_map_comap f).u_top

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

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

Разделы

Аффилиация

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