English
Induction principle on PiTensorProduct states that any element can be built from scaled tprod pieces via addition.
Русский
Индукционный принцип для PiTensorProduct: любой элемент строится из масштабируемых частей tprod через сложение.
LaTeX
$$$$ \text{PiTensorProduct.induction_on}(z,smul_tprod,add) = \text{motive } z $$$$
Lean4
/-- Auxiliary function to constructing a linear map `(⨂[R] i, s i) → E` given a
`MultilinearMap R s E` with the property that its composition with the canonical
`MultilinearMap R s (⨂[R] i, s i)` is the given multilinear map. -/
def liftAux (φ : MultilinearMap R s E) : (⨂[R] i, s i) →+ E :=
liftAddHom (fun p : R × Π i, s i ↦ p.1 • φ p.2) (fun z f i hf ↦ by simp_rw [map_coord_zero φ i hf, smul_zero])
(fun f ↦ by simp_rw [zero_smul]) (fun z f i m₁ m₂ ↦ by simp_rw [← smul_add, φ.map_update_add])
(fun z₁ z₂ f ↦ by rw [← add_smul]) fun z f i r ↦ by simp [φ.map_update_smul, smul_smul, mul_comm]
