English
The continuous multilinear map on A^ι with fixed coordinate product exists for ι finite; it sends m to ∏ i m_i, and toMultilinearMap is MultilinearMap.mkPiAlgebraFin.
Русский
Существование непрерывного мультилінійного отображения на A^ι для конечного множества координат; отображение отправляет m в произведение координат.
LaTeX
$$ContinuousMultilinearMap.mkPiAlgebraFin R n A m = ∏ i, m_i$$
Lean4
/-- The continuous multilinear map on `A^n`, where `A` is a normed algebra over `𝕜`, associating to
`m` the product of all the `m i`.
See also: `ContinuousMultilinearMap.mkPiAlgebra`. -/
protected def mkPiAlgebraFin : A [×n]→L[R] A
where
cont := by
change Continuous fun m => (List.ofFn m).prod
simp_rw [List.ofFn_eq_map]
exact continuous_list_prod _ fun i _ => continuous_apply _
toMultilinearMap := MultilinearMap.mkPiAlgebraFin R n A
