Theorems · Theorem · functional analysis

ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv

∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] [SeparatingDual 𝕜 V]
  [SeparatingDual 𝕜 W] (f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W), ∃ U, f = U.conjContinuousAlgEquiv

This is the continuous version of AlgEquiv.eq_linearEquivConjAlgEquiv.

Defined in

Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupSeminormedAddCommGroupNormedSpaceNormedSpaceSeparatingDualSeparatingDual