mkQ_map_self

Mathlib.LinearAlgebra.Quotient.Basic

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

English

The map p.mkQ from p to itself is the zero map, i.e., map p.mkQ p = ⊥.

Русский

Отображение p.mkQ отображает p в себя как нулевое: map p.mkQ p = ⊥.

LaTeX

$$$$ \\operatorname{map} \\bigl(p.mkQ\\bigr) p = \\bot. $$$$

Lean4

@[simp]
theorem mkQ_map_self : map p.mkQ p = ⊥ := by rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]

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

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

Разделы

Аффилиация

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