eval

Mathlib.Tactic.Module

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Module.NF.eval

Lean4

/-- Evaluate a `Module.NF R M` object `l`, i.e. a list of pairs in `R × M`, to an element of `M`, by
forming the "linear combination" it specifies: scalar-multiply each `R` term to the corresponding
`M` term, then add them all up. -/
def eval [Add M] [Zero M] [SMul R M] (l : NF R M) : M :=
  (l.map (fun (⟨r, x⟩ : R × M) ↦ r • x)).sum

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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