lift_tprod

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.lift_tprod

English

The lift of the tprod multilinear map equals the identity map on the PiTensorProduct.

Русский

Поднятие тензорного произведения (tprod) равно тождественному отображению на PiTensorProduct.

LaTeX

$$$ lift(tprod_R) = \mathrm{LinearMap.id} $$$

Lean4

@[simp]
theorem lift_tprod : lift (tprod R : MultilinearMap R s _) = LinearMap.id :=
  Eq.symm <| lift.unique' rfl

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

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

Разделы

Аффилиация

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