map_smul_univ — Mathlib

English

If two continuous multilinear maps f and g over R on (ι → R) are equal when evaluated at the all-ones vector, then f = g.

Русский

Если две непрерывные мультилінійні отображения совпадают на единичном векторе, то они равны.

LaTeX

$$f(1,1,...,1) = g(1,1,...,1) ⇒ f = g$$

Lean4

/-- Multiplicativity of a continuous multilinear 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 : ∀ i, M₁ i) : (f fun i => c i • m i) = (∏ i, c i) • f m :=
  f.toMultilinearMap.map_smul_univ _ _

Похожие утверждения