mkPiRing — Mathlib

English

The canonical continuous multilinear map on R^ι to M sends m to (∏ i m_i) • z for a fixed z ∈ M.

Русский

Каноническое непрерывное мультиляйнерное отображение на R^ι, которое отправляет m в (∏ i m_i) • z.

LaTeX

$$mkPiRing R ι z : (ι → R) → M with (mkPiRing R ι z)(m) = (∏ i, m_i) • z$$

Lean4

/-- The canonical continuous multilinear map on `R^ι`, associating to `m` the product of all the
`m i` (multiplied by a fixed reference element `z` in the target module) -/
protected def mkPiRing (z : M) : ContinuousMultilinearMap R (fun _ : ι => R) M :=
  (ContinuousMultilinearMap.mkPiAlgebra R ι R).smulRight z

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