coe_pi — Mathlib

English

There is a general IsScalarTower instance for ContinuousMultilinearMap with respect to two scalar rings.

Русский

Существует общий экземпляр IsScalarTower для ContinuousMultilinearMap относительно двух колец скаляров.

LaTeX

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

Lean4

@[simp]
theorem coe_pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
    [∀ i, Module R (M' i)] (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) : ⇑(pi f) = fun m j => f j m :=
  rfl

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