fst_prod

Mathlib.LinearAlgebra.Prod

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

English

The first projection composed with the product map equals the first component map: (fst) ∘ (f.prod g) = f.

Русский

Сведение первой проекции к произведению отображений даёт исходную карту f: (fst) ∘ (f.prod g) = f.

LaTeX

$$$ (fst\;R\;M_2\;M_3).comp (f.prod\ g) = f $$$

Lean4

@[simp]
theorem fst_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : (fst R M₂ M₃).comp (prod f g) = f :=
  rfl

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

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

Разделы

Аффилиация

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