Theorems · Theorem · functional analysis

ContinuousLinearEquiv.conjContinuousAlgEquiv_trans

∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup E] [inst_1 : AddCommGroup G]
  [inst_2 : AddCommGroup H] [inst_3 : NormedField 𝕜] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 G] [inst_6 : Module 𝕜 H]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace G] [inst_9 : TopologicalSpace H]
  [inst_10 : IsTopologicalAddGroup G] [inst_11 : IsTopologicalAddGroup H] [inst_12 : ContinuousConstSMul 𝕜 G]
  [inst_13 : ContinuousConstSMul 𝕜 H] [inst_14 : IsTopologicalAddGroup E] [inst_15 : ContinuousConstSMul 𝕜 E]
  (e : E ≃L[𝕜] G) (f : G ≃L[𝕜] H),
  (e.trans f).conjContinuousAlgEquiv = e.conjContinuousAlgEquiv.trans f.conjContinuousAlgEquiv

Defined in

Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupAddCommGroupAddCommGroupNormedFieldModuleModuleModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupIsTopologicalAddGroupContinuousConstSMulContinuousConstSMulIsTopologicalAddGroupContinuousConstSMul