lapply_comp_lsingle_of_ne

Mathlib.LinearAlgebra.DFinsupp

URI: https://scilib.ai/kg/mathlib#DFinsupp.lapply_comp_lsingle_of_ne

← MathLib Explorer

English

If i ≠ i', then lapply_i composed with lsingle_{i'} is the zero map.

Русский

Если i ≠ i', то lapply_i ∘ lsingle_{i'} = 0.

LaTeX

$$$i \\neq i' \\Rightarrow \\mathrm{lapply}\\,i \\circ \\mathrm{lsingle}\\,i' = 0$$$

Lean4

@[simp]
theorem lapply_comp_lsingle_of_ne [DecidableEq ι] (i i' : ι) (h : i ≠ i') :
    lapply i ∘ₗ lsingle i' = (0 : M i' →ₗ[R] M i) := by ext; simp [h.symm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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