coprod_zero_left

Mathlib.LinearAlgebra.Prod

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

English

Equivalent restatement of the previous fact using a transfer lemma.

Русский

Эквивалентное переформулирование предыдущей вещи через вспомогательную лемму переноса.

LaTeX

$$$ (f\\circ (inl\\ R\\ M\\ M_2)).coprod (f\\circ (inr\\ R\\ M\\ M_2)) = f $$$

Lean4

theorem coprod_zero_left (g : M₂ →ₗ[R] M₃) : (0 : M →ₗ[R] M₃).coprod g = g.comp (snd R M M₂) :=
  zero_add _

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

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

Разделы

Аффилиация

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