English
Two families of linear isomorphisms e_i : M_i ≃ M_i' induce a linear equivalence between the corresponding spaces of multilinear maps: MultilinearMap R M1' M2 ≃ₗ[R] MultilinearMap R M1 M2.
Русский
Две семьи линейных изоморфизмов e_i : M_i ≃ M_i' порождают линейное эквивалентное отображение между пространствами мультиляйнерных отображений: MultilinearMap R M1' M2 ≃ₗ[R] MultilinearMap R M1 M2.
LaTeX
$$$$\text{LinearEquiv}_{\text{multilinearMapCongrLeft}}(e) : (MultilinearMap\;R\;M_1'\;M_2) \simeq_{\text{linear}} (MultilinearMap\;R\;M_1\;M_2).$$$$
Lean4
/-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear
map is multiplied by `∏ i ∈ s, c i`. This is mainly an auxiliary statement to prove the result when
`s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not
require the index set `ι` to be finite. -/
theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m :=
by
refine s.induction_on (by simp) ?_
intro j s j_notMem_s Hrec
have A : Function.update (s.piecewise (fun i => c i • m i) m) j (m j) = s.piecewise (fun i => c i • m i) m :=
by
ext i
by_cases h : i = j
· rw [h]
simp [j_notMem_s]
· simp [h]
rw [s.piecewise_insert, f.map_update_smul, A, Hrec]
simp [j_notMem_s, mul_smul]
