comap_bot

Mathlib.Algebra.Module.Submodule.Ker

URI: https://scilib.ai/kg/mathlib#Submodule.comap_bot

English

The kernel of f is exactly the preimage of 0 under f, i.e., ker f = comap f ⊥.

Русский

Ядро f равно прообразу нуля под действием f: ker f = comap f ⊥.

LaTeX

$$$\ker f = \operatorname{comap} f \perp$$$

Lean4

@[simp]
theorem comap_bot (f : F) : comap f ⊥ = ker f :=
  rfl

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

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

Разделы

Аффилиация

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