lift_symm

Mathlib.LinearAlgebra.PiTensorProduct

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

English

Theorem unique' (restated): if H holds that φ'.compMultilinearMap (tprod R) = φ, then φ' = lift φ.

Русский

Теорема unique' (переформулированная): если H выполняется, что φ'.compMultilinearMap (tprod R) = φ, то φ' = lift φ.

LaTeX

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

Lean4

@[simp]
theorem lift_symm (φ' : (⨂[R] i, s i) →ₗ[R] E) : lift.symm φ' = φ'.compMultilinearMap (tprod R) :=
  rfl

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

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

Разделы

Аффилиация

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