mkPiAlgebra — Mathlib

English

For m : Fin n → A, mkPiAlgebraFin R n A m equals the product ∏ i m_i.

Русский

Для m : Fin n → A выполняется mkPiAlgebraFin R n A m = ∏ i m_i.

LaTeX

$$mkPiAlgebraFin R n A m = ∏ i, m_i$$

Lean4

/-- The continuous multilinear map on `A^ι`, where `A` is a normed commutative algebra
over `𝕜`, associating to `m` the product of all the `m i`.

See also `ContinuousMultilinearMap.mkPiAlgebraFin`. -/
protected def mkPiAlgebra : ContinuousMultilinearMap R (fun _ : ι => A) A
    where
  cont := continuous_finset_prod _ fun _ _ => continuous_apply _
  toMultilinearMap := MultilinearMap.mkPiAlgebra R ι A

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