toContinuousMultilinearMapCLM — Mathlib

English

Restriction of scalars map remains an embedding, preserving the topological and uniform structure when passing to 𝕜'.

Русский

Отображение ограничения скаляров сохраняет вложение и топологическую/однородную структуру при переходе к 𝕜'.

LaTeX

$$$\\text{IsEmbedding}(\\operatorname{restrictScalars}_{\\mathbb{k}'})$$$

Lean4

/-- The inclusion of *alternating* continuous multi-linear maps into continuous multi-linear maps
as a continuous linear map. -/
@[simps! -fullyApplied]
def toContinuousMultilinearMapCLM (R : Type*) [Semiring R] [Module R F] [ContinuousConstSMul R F]
    [SMulCommClass 𝕜 R F] : E [⋀^ι]→L[𝕜] F →L[R] ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F :=
  ⟨toContinuousMultilinearMapLinear, continuous_induced_dom⟩

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