coprod

Mathlib.LinearAlgebra.Prod

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

← MathLib Explorer

English

The composition of coprod f g with inl equals f: (coprod f g) ∘ inl = f.

Русский

Композиция coprod f g с inl равна f: (coprod f g) ∘ inl = f.

LaTeX

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

Lean4

/-- The coprod function `x : M × M₂ ↦ f x.1 + g x.2` is a linear map. -/
def coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : M × M₂ →ₗ[R] M₃ :=
  f.comp (fst _ _ _) + g.comp (snd _ _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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