ofDirectSum_comp_toDirectSum

Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

URI: https://scilib.ai/kg/mathlib#TensorAlgebra.ofDirectSum_comp_toDirectSum

English

The composition of ofDirectSum followed by toDirectSum is the identity on the direct sum.

Русский

Композиция ofDirectSum ∘ toDirectSum есть тождественное отображение на прямой сумме.

LaTeX

$$$ ofDirectSum.comp toDirectSum = AlgHom.id R (\bigoplus_n ⨂[R]^n M) $$$

Lean4

theorem ofDirectSum_comp_toDirectSum : ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M) :=
  by
  ext
  simp [tprod_apply]

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

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

Разделы

Аффилиация

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