compContinuousMultilinearMap_coe — Mathlib

English

If R'ᵐᵒᵖ and IsScalarTower structure with CMMap is given, then there is a IsScalarTower instance for CMMap with these rings.

Русский

Существует инстанс IsScalarTower для CMMap над R'ᵐᵒᵖ и R'' с учётом условий.

LaTeX

$$$\\text{IsScalarTower } R'^\mathrm{op} R'' (\\mathrm{ContinuousMultilinearMap} A M_1 M_2)$$$

Lean4

@[simp]
theorem _root_.ContinuousLinearMap.compContinuousMultilinearMap_coe (g : M₂ →L[R] M₃)
    (f : ContinuousMultilinearMap R M₁ M₂) :
    (g.compContinuousMultilinearMap f : (∀ i, M₁ i) → M₃) = (g : M₂ → M₃) ∘ (f : (∀ i, M₁ i) → M₂) :=
  by
  ext m
  rfl

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