lc — Mathlib · SciLib

English

The function lc is exactly the same as the standard Finsupp.linearCombination construction; i.e., lc e l = Finsupp.linearCombination R e l.

Русский

Функция lc идентична обычной конструкции Finsupp.linearCombination; то есть lc e l = Finsupp.linearCombination R e l.

LaTeX

$$$ lc\\ e\\ l = Finsupp.linearCombination R\\ e\\ l $$$

Lean4

/-- linear combinations of elements of `e`.
This is a convenient abbreviation for `Finsupp.linearCombination R e l` -/
def lc {ι} (e : ι → M) (l : ι →₀ R) : M :=
  l.sum fun (i : ι) (a : R) => a • e i

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