English
If one multiplies coordinates indexed by a finite set s by factors c_i, the image under the multilinear map is multiplied by the product of c_i over i in s.
Русский
Если коэффициентов в координатах, индексируемых конечным множеством s, умножить на c_i, то изображение мультиленейного отображения умножится на произведение c_i по i ∈ s.
LaTeX
$$$$f( s\text{ piecewise } (c_i \cdot m_i) ) = \Big(\prod_{i \in s} c_i\Big) f(m).$$$$
Lean4
@[simp]
theorem map_update_smul_left [DecidableEq ι] [Fintype ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x) :=
by
have :
f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
(∏ _i ∈ Finset.univ.erase i, c) • f (update m i x) :=
map_piecewise_smul f _ _ _
simpa [← Function.update_smul c m] using this
