Theorems · Definition · functional analysis
WithCStarModule.equiv
(A : Type u_3) → (E : Type u_4) → WithCStarModule A E ≃ E
The canonical equivalence between C⋆ᵐᵒᵈ(A, E) and E. This should always be used to
convert back and forth between the representations.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Equiv.reflproof · cited by 274
- WithCStarModulestatement and proof · cited by 66
Cited by36
Results whose statement or proof uses this declaration.
- WithCStarModule.linearEquivproof · cited by 3
- CStarMatrix.toCLM_apply_singlestatement · cited by 2
- CStarMatrix.toCLM_apply_single_applystatement · cited by 2
- CStarMatrix.inner_toCLM_conjTranspose_leftproof · cited by 1
- WithCStarModule.inner_single_leftstatement · cited by 1
- WithCStarModule.inner_single_rightstatement · cited by 1
- WithCStarModule.norm_singlestatement and proof · cited by 1
- CStarMatrix.toCLM_apply_eq_sumstatement · cited by 1
- CStarMatrix.toCLM_injectiveproof · cited by 1
- WithCStarModule.addEquivproof · cited by 0
- WithCStarModule.equivL_applystatement · cited by 0
- WithCStarModule.equivL_symm_applystatement · cited by 0