constr_def — Mathlib

English

The construction constr is the linear map built from the data f and the basis via lmapDomain and linearCombination.

Русский

Конструкция constr является линейным отображением, построенным из данных f и базиса через lmapDomain и линейную комбинацию.

LaTeX

$$$\\mathrm{constr} = ( \\mathrm{Finsupp.linearCombination\\} R\\ id) \\circ ( \\mathrm{Finsupp.lmapDomain}\\, R\\, R\\ f) \\circ \\uparrow b.\\mathrm{repr}$$$

Lean4

theorem constr_def (f : ι → M') :
    constr (M' := M') b S f = linearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr :=
  rfl

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