fst_eq_coprod

Mathlib.LinearAlgebra.Prod

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

English

The second projection equals the coprod of the zero map and the identity on M₂: snd = 0 × id.

Русский

Вторая проекция равна копродукту нулевого отображения и тождества на M₂: snd = 0 × id.

LaTeX

$$$ snd\\, R\\, M\\, M_2 = coprod\\, 0\\, id $$$

Lean4

theorem fst_eq_coprod : fst R M M₂ = coprod LinearMap.id 0 := by ext; simp

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

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

Разделы

Аффилиация

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