range_mkQ_comp

Mathlib.LinearAlgebra.Quotient.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.range_mkQ_comp

English

The map from the range of f to the quotient M₂ is zero when composed with mkQ, i.e., the image of the range under mkQ is zero.

Русский

Образ отображения mkQ композитом с range f равен нулю: (range f).mkQ ∘ f = 0.

LaTeX

$$$$ (range\\, f).mkQ \\circ f = 0. $$$$

Lean4

theorem range_mkQ_comp (f : M →ₛₗ[τ₁₂] M₂) : (range f).mkQ.comp f = 0 :=
  LinearMap.ext fun x => by simp

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

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

Разделы

Аффилиация

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