coeFnLinearMap — Mathlib

English

There is a natural linear map from the direct sum to the pi-type, called coeFnLinearMap, sending an element to its family of components.

Русский

Существует естественное линейное отображение из прямой суммы в произведение по индексам, названное coeFnLinearMap, отправляющее элемент в его семейство компонент.

LaTeX

$$$\\mathrm{coeFnLinearMap\\;R}: (\\bigoplus_{i} M_i) \\to_{{R}} (i \\mapsto M_i).$$$

Lean4

/-- Coercion from a `DirectSum` to a pi type is a `LinearMap`. -/
def coeFnLinearMap : (⨁ i, M i) →ₗ[R] ∀ i, M i :=
  DFinsupp.coeFnLinearMap R

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