toModule — Mathlib

English

The universal property of the coproduct gives a linear map to N from the direct sum determined by the family φ i: M_i → N.

Русский

Универсальное свойство копрокопродукта задаёт линейное отображение из прямой суммы в N, определённое семейством $φ_i$.

LaTeX

$$$\\mathrm{toModule}\\; R\\; ι\\; N\\; φ : (\\bigoplus_i M_i) \\to_{{R}} N.$$$

Lean4

/-- The linear map constructed using the universal property of the coproduct. -/
def toModule : (⨁ i, M i) →ₗ[R] N :=
  DFunLike.coe (DFinsupp.lsum ℕ) φ

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