proj_comp_single_ne

Mathlib.LinearAlgebra.Pi

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

English

If i ≠ j, then the composition proj_i ∘ single_j is the zero map.

Русский

Если i ≠ j, то композиция proj_i ∘ single_j — нулевое отображение.

LaTeX

$$$(\\mathrm{proj}_i) \\circ (\\text{single } R \\; \\varphi \\; j) = 0 \\quad \\text{если } i \\neq j.$$$

Lean4

theorem proj_comp_single_ne (i j : ι) (h : i ≠ j) : (proj i).comp (single R φ j) = 0 :=
  LinearMap.ext <| Pi.single_eq_of_ne h

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

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

Разделы

Аффилиация

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