Theorems · Theorem · functional analysis

ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iff

∀ {R : Type u_4} {V : Type u_5} {W : Type u_6} [inst : NormedField R] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup W] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace W]
  [IsTopologicalRing R] [inst_7 : Module R V] [inst_8 : Module R W] [SeparatingDual R V]
  [inst_10 : IsTopologicalAddGroup V] [inst_11 : IsTopologicalAddGroup W] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] (f g : V ≃L[R] W), f.conjContinuousAlgEquiv = g.conjContinuousAlgEquiv ↔ ∃ α, f = α • g

Defined in

Mathlib.Analysis.LocallyConvex.SeparatingDual

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupAddCommGroupTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalRingModuleModuleSeparatingDualIsTopologicalAddGroupIsTopologicalAddGroupContinuousSMulContinuousSMul