toMultilinearMapLinear — Mathlib

English

There is a canonical continuous multilinear map on A^ι (finite index set) given by the product of all coordinates, i.e., (mkPiAlgebraFin R n A) m = ∏ i m_i.

Русский

Существует каноническое непрерывное мультинейральное отображение на A^ι, заданное произведением всех координат.

LaTeX

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

Lean4

/-- Linear map version of the map `toMultilinearMap` associating to a continuous multilinear map
the corresponding multilinear map. -/
@[simps]
def toMultilinearMapLinear : ContinuousMultilinearMap A M₁ M₂ →ₗ[R'] MultilinearMap A M₁ M₂
    where
  toFun := toMultilinearMap
  map_add' := toMultilinearMap_add
  map_smul' := toMultilinearMap_smul

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