Theorems · Definition · functional analysis
WithCStarModule
Type u_1 → Type u_2 → Type u_2
A type synonym for endowing a given type with a CStarModule structure. This has the scoped
notation C⋆ᵐᵒᵈ.
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by75
Results whose statement or proof uses this declaration.
- WithCStarModule.equivstatement and proof · cited by 33
- CStarMatrix.toCLMstatement · cited by 13
- WithCStarModule.extstatement and proof · cited by 3
- WithCStarModule.linearEquivstatement and proof · cited by 3
- WithCStarModule.equivLstatement and proof · cited by 2
- WithCStarModule.norm_apply_le_normstatement and proof · cited by 2
- WithCStarModule.pi_norm_sqstatement and proof · cited by 2
- CStarMatrix.toCLMNonUnitalAlgHomstatement and proof · cited by 2
- CStarMatrix.toCLM_apply_singlestatement and proof · cited by 2
- CStarMatrix.toCLM_apply_single_applystatement · cited by 2
- WithCStarModule.inner_single_leftstatement and proof · cited by 1
- WithCStarModule.inner_single_rightstatement and proof · cited by 1