Theorems · Definition · functional analysis

AlgHom.toContinuousLinearMap

{𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NormedRing A] → [inst_2 : NormedAlgebra 𝕜 A] → [CompleteSpace A] → (A →ₐ[𝕜] 𝕜) → StrongDual 𝕜 A

An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

3 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldNormedRingNormedAlgebraCompleteSpace