English
Let f be a continuous R-alternating map M^{ι} → N. For any scalars c_i ∈ R and vectors m_i ∈ M (i ∈ ι), the value of f at the coordinate-wise scaled inputs equals the product of the scalars times f at the original inputs: f(i ↦ c_i · m_i) = (∏_{i∈ι} c_i) · f(m).
Русский
Пусть f — непрерывное R-альтернирующее отображение M^{ι} → N. Для любых скаляров c_i ∈ R и векторов m_i ∈ M (по i ∈ ι) значение f на входах, полученных путём одновременного масштабирования координат, равно произведению всех скаляров, умноженному на f(м) исходных входов: f(i ↦ c_i · m_i) = (∏_{i∈ι} c_i) · f(m).
LaTeX
$$$$f\\bigl( (c_i m_i)_{i\\in\\iota} \\bigr) = \\Bigl(\\prod_{i\\in\\iota} c_i\\Bigr)\\, f\\bigl( (m_i)_{i\\in\\iota} \\bigr).$$$$
Lean4
/-- Multiplicativity of a continuous alternating map along all coordinates at the same time,
writing `f (fun i ↦ c i • m i)` as `(∏ i, c i) • f m`. -/
theorem map_smul_univ [Fintype ι] (c : ι → R) (m : ι → M) : (f fun i => c i • m i) = (∏ i, c i) • f m :=
f.toMultilinearMap.map_smul_univ _ _
