liftAux_tprodCoeff

Mathlib.LinearAlgebra.PiTensorProduct

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

English

liftAux φ applied to tprod f equals φ f.

Русский

liftAux φ применённый к tprod f равен φ f.

LaTeX

$$$$ \text{liftAux}(\phi)(tprod(R,f)) = φ(f) $$$$

Lean4

theorem liftAux_tprodCoeff (φ : MultilinearMap R s E) (z : R) (f : Π i, s i) : liftAux φ (tprodCoeff R z f) = z • φ f :=
  rfl

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

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

Разделы

Аффилиация

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