single_eq_lof

Mathlib.Algebra.DirectSum.Module

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

English

The DFinsupp single on index i with value b is equal to lof_i(b).

Русский

DFinsupp.single на индексе i со значением b равен lof_i(b).

LaTeX

$$$\\mathrm{DFinsupp}.\\mathrm{single}\\; i\\; b = \\mathrm{lof}\\; R\\; ι\\; M\\; i\\; b$$$

Lean4

theorem single_eq_lof (i : ι) (b : M i) : DFinsupp.single i b = lof R ι M i b :=
  rfl

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

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

Разделы

Аффилиация

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