lof_apply

Mathlib.Algebra.DirectSum.Module

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

English

The left-embedding lof_i: M_i → ⊕_i M_i has its i-th component equal to the original element.

Русский

Вложение в лево lof_i: M_i → ⊕_i M_i имеет i-ю координату равной исходному элементу.

LaTeX

$$$((\\mathrm{lof}\\,i\\,b))_i = b.$$$

Lean4

@[simp]
theorem lof_apply [DecidableEq ι] (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
  DFinsupp.single_eq_same

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

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

Разделы

Аффилиация

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