tprod

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.lift.tprod

English

Theorem unique' states that if φ' is such that φ'.compMultilinearMap (tprod R) = φ, then φ' = lift φ.

Русский

Теорема unique': если φ' удовлетворяет φ'.compMultilinearMap (tprod R) = φ, то φ' = lift φ.

LaTeX

$$$$ \text{unique'}(H) : φ' = \text{lift } φ $$$$

Lean4

@[simp]
theorem tprod (f : Π i, s i) : lift φ (tprod R f) = φ f :=
  liftAux_tprod φ f

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

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

Разделы

Аффилиация

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