smul — Mathlib

English

The symmetric form of lift, i.e., the inverse of lift, is given by taking the composition with tprod.

Русский

Симметричная форма lift, то есть обратная к lift, задаётся через композицию с tprod.

LaTeX

$$$$ \text{lift.symm}(\phi') = \phi'\circ\operatorname{MultilinearMap}(tprod) $$$$

Lean4

theorem smul {φ : MultilinearMap R s E} (r : R) (x : ⨂[R] i, s i) : liftAux φ (r • x) = r • liftAux φ x :=
  by
  refine PiTensorProduct.induction_on' x ?_ ?_
  · intro z f
    rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
  · intro z y ihz ihy
    rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]

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