English
Scalar multiplication commutes with currySum: currySum(r • f) = r • currySum(f).
Русский
Скалярное умножение коммутирует с currySum: currySum(r • f) = r • currySum(f).
LaTeX
$$$\\text{currySum}(r \\cdot f) = r \\cdot \\text{currySum}(f)$$$
Lean4
/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))` induces a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces. -/
def uncurrySum (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
MultilinearMap R N M₂ where
toFun u := g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i'))
map_update_add' := by
letI := Classical.decEq ι
letI := Classical.decEq ι'
rintro _ _ (_ | _) _ _ <;> simp
map_update_smul' := by
letI := Classical.decEq ι
letI := Classical.decEq ι'
rintro _ _ (_ | _) _ _ <;> simp
