liftQ_mkQ

Mathlib.LinearAlgebra.Quotient.Basic

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

English

Reiterating: if P < ⊤, then M / P is nontrivial.

Русский

Повторное утверждение: если P < ⊤, тогда M / P не тривиален.

LaTeX

$$$$ P < \\top \\Rightarrow \\operatorname{Nontrivial}(M / P). $$$$

Lean4

@[simp]
theorem liftQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) (h) : (p.liftQ f h).comp p.mkQ = f := by ext; rfl

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

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

Разделы

Аффилиация

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