lmk — Mathlib

English

The lmk construction builds the direct sum from a finite family of modules indexed by a finite set.

Русский

Конструкция lmk восстанавливает прямую сумму из конечной семьи модулей, индексированной по конечному множеству.

LaTeX

$$$\\mathrm{lmk}:\\, \\forall s:\\mathrm{Finset}\\; ι\\;,\\; (\\forall i\\in s, M_i) \\to_{{R}} \\bigoplus_i M_i.$$$

Lean4

/-- Create the direct sum given a family `M` of `R` modules indexed over `ι`. -/
def lmk : ∀ s : Finset ι, (∀ i : (↑s : Set ι), M i.val) →ₗ[R] ⨁ i, M i :=
  DFinsupp.lmk

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