lof

Mathlib.Algebra.DirectSum.Module

URI: https://scilib.ai/kg/mathlib#DirectSum.lof

English

For each index i, there is an inclusion map from M_i into the direct sum ⨁ i, M_i.

Русский

Для каждого индекса i существует включающее отображение из M_i в прямую сумму ⨁ i, M_i.

LaTeX

$$$\\mathrm{lof}:\\; \\forall i, M_i \\to_{{R}} \\bigoplus_i M_i.$$$

Lean4

/-- Inclusion of each component into the direct sum. -/
def lof : ∀ i : ι, M i →ₗ[R] ⨁ i, M i :=
  DFinsupp.lsingle

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

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

Разделы

Аффилиация

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