toCLM — Mathlib

English

Each character in the space corresponds to a continuous linear map from A to 𝕜.

Русский

Каждый элемент пространства характеристик соответствует непрерывному линейному отображению $A \\to 𝕜$.

LaTeX

$$$\\text{toCLM }(φ) : A \\toL[𝕜] 𝕜$$$

Lean4

/-- An element of the character space, as a continuous linear map. -/
def toCLM (φ : characterSpace 𝕜 A) : A →L[𝕜] 𝕜 :=
  (φ : WeakDual 𝕜 A)

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