mapLMonoidHom — Mathlib

English

The monoid-hom structure for mapL is compatible with composition and units, via the same defining mapL.

Русский

Структура моноида для mapL совместима с композициями и единицей через ту же задающую mapL.

LaTeX

$$$ (\\mathrm{mapLMonoidHom}\; ) : (\\Pi i, E_i \\toL[𝕜] E_i) \\to* ((⨂[𝕜] i, E_i) \\toL[𝕜] ⨂[𝕜] i, E_i) $$$

Lean4

/-- Upgrading `PiTensorProduct.mapL` to a `MonoidHom` when `E = E'`. -/
@[simps]
noncomputable def mapLMonoidHom : (Π i, E i →L[𝕜] E i) →* ((⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E i)
    where
  toFun := mapL
  map_one' := mapL_one
  map_mul' := mapL_mul

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