lof_self

Mathlib.Algebra.DirectSum.Module

URI: https://scilib.ai/kg/mathlib#DirectSum.component.lof_self

English

The i-th component of lof_i(b) is b.

Русский

i-я компонента lof_i(b) равна b.

LaTeX

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

Lean4

@[simp]
theorem lof_self [DecidableEq ι] (i : ι) (b : M i) : component R ι M i ((lof R ι M i) b) = b :=
  lof_apply R i b

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

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

Разделы

Аффилиация

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