English
liftAux φ is the additive homomorphism constructing a map (⨂[R] i, s i) → E from a multilinear map φ, with the property that its action on simple tensors matches φ on the arguments.
Русский
liftAux φ — это добавочное гомоморфное отображение, строящее отображение из тензорного произведения в E из многоэллиптического φ, при этом на простых тензорах оно совпадает с φ.
LaTeX
$$$$ \operatorname{liftAux}(\phi): (⨂[R] i, s i) \to+ E \quad \text{ s.t. } \operatorname{liftAux}(\phi)(a \otimes m) = a · φ(m) $$$$
Lean4
theorem liftAux_tprod (φ : MultilinearMap R s E) (f : Π i, s i) : liftAux φ (tprod R f) = φ f :=
by
simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk']
-- The end of this proof was very different before https://github.com/leanprover/lean4/pull/2644:
-- rw [FreeAddMonoid.of, FreeAddMonoid.ofList, Equiv.refl_apply, AddCon.lift_coe]
-- dsimp [FreeAddMonoid.lift, FreeAddMonoid.sumAux]
-- show _ • _ = _
-- rw [one_smul]
erw [AddCon.lift_coe]
simp
