snd_eq_coprod

Mathlib.LinearAlgebra.Prod

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

English

Replacing the left map by zero in coprod yields the right map composed with snd: (0) ⊔ g = g ∘ snd.

Русский

Замена левого отображения нулём в coprod даёт отображение g после snd: (0) coprod g = g ∘ snd.

LaTeX

$$$ (0 : M \\to M_3)\\coprod g = g \\circ (snd\\ R\\ M\\ M_2) $$$

Lean4

theorem snd_eq_coprod : snd R M M₂ = coprod 0 LinearMap.id := by ext; simp

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

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

Разделы

Аффилиация

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