decompose_symm_of

Mathlib.Algebra.DirectSum.Decomposition

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

English

For x in the i-th component, the decomposition equals the i-th injection of x.

Русский

Для x в i-й компоненте разложение даёт i-ю инъекцию x.

LaTeX

$$$\mathrm{decompose}_{\mathcal{M}}(x) = \mathrm{DirectSum.of}_{i}(x)$$$

Lean4

@[simp]
theorem decompose_symm_of {i : ι} (x : ℳ i) : (decompose ℳ).symm (DirectSum.of _ i x) = x :=
  DirectSum.coeAddMonoidHom_of ℳ _ _

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

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

Разделы

Аффилиация

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