lapply_comp_lsingle_same

Mathlib.LinearAlgebra.DFinsupp

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

English

For any i, lapply_i composed with lsingle_i is the identity on M_i.

Русский

Для любого i композиция lapply_i и lsingle_i равна тождественному отображению на M_i.

LaTeX

$$$\\bigl(\\mathrm{lapply}\\,i\\bigr)\\circ\\mathrm{lsingle}\\,i = \\mathrm{id}_{M_i}$$$

Lean4

@[simp]
theorem lapply_comp_lsingle_same [DecidableEq ι] (i : ι) : lapply i ∘ₗ lsingle i = (.id : M i →ₗ[R] M i) := by ext; simp

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

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

Разделы

Аффилиация

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