proj_comp_single_same

Mathlib.LinearAlgebra.Pi

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

English

For a fixed i, the composition proj_i ∘ single_i is the identity on φ_i.

Русский

Для фиксированного i композиция proj_i ∘ single_i равна тождественному отображению на φ_i.

LaTeX

$$$(\\mathrm{proj}_i) \\circ (\\text{single } R \\; \\varphi \\; i) = \\mathrm{id}_{\\phi_i}.$$$

Lean4

theorem proj_comp_single_same (i : ι) : (proj i).comp (single R φ i) = id :=
  LinearMap.ext <| Pi.single_eq_same i

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

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

Разделы

Аффилиация

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