of_eq_same

Mathlib.Algebra.DirectSum.Basic

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

English

The coefficient of the i-th component in the i-th summand equals the original value.

Русский

Коэффициент в i-й компоненте в i-й слагаемой равен исходному значению.

LaTeX

$$$(DirectSum.of\\;β\\;i\\;x)_i = x$$$

Lean4

@[simp]
theorem of_eq_same (i : ι) (x : β i) : (of _ i x) i = x :=
  DFinsupp.single_eq_same

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

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

Разделы

Аффилиация

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