le_comap_mkQ

Mathlib.LinearAlgebra.Quotient.Basic

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

English

For any p' ⊆ M ⧸ p, we have p ≤ comap p.mkQ p'.

Русский

Для любого p' ⊆ M ⧸ p имеем p ≤ comap p.mkQ p'.

LaTeX

$$$$ p \\le \\operatorname{comap}_{p.mkQ} p'. $$$$

Lean4

theorem le_comap_mkQ (p' : Submodule R (M ⧸ p)) : p ≤ comap p.mkQ p' := by
  simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

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

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

Разделы

Аффилиация

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