prod_map_snd

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#Submodule.prod_map_snd

English

The map of the product p × q by fst is p: (p × q).map fst = p.

Русский

Образ произведения p × q под fst равен p: (p × q).map fst = p.

LaTeX

$$$(\\mathrm{prod}\\, p\\, q).\\mathrm{map}(\\mathrm{fst}\\, R\\, M\\, M_2) = p$$$

Lean4

@[simp]
theorem prod_map_snd : (prod p q).map (snd R M M₂) = q := by ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ p)]

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

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

Разделы

Аффилиация

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