Theorems · Definition · functional analysis
CStarMatrix
Type u_1 → Type u_2 → Type u_3 → Type (max u_1 u_2 u_3)
Type copy Matrix m n A meant for matrices with entries in a C⋆-algebra. This is
a C⋆-algebra when m = n.
- Cited by
- 67 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrixproof · cited by 4,303
Cited by89
Results whose statement or proof uses this declaration.
- CStarMatrix.toCLMstatement and proof · cited by 13
- CStarMatrix.mapstatement and proof · cited by 12
- CStarMatrix.ofMatrixstatement · cited by 10
- CStarMatrix.extstatement and proof · cited by 4
- CStarMatrix.mapₗstatement and proof · cited by 4
- CStarMatrix.reindexₐstatement and proof · cited by 4
- CStarMatrix.conjTransposestatement and proof · cited by 3
- CStarMatrix.ext_iffstatement 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 and proof · cited by 2
- CStarMatrix.conjTranspose_applystatement and proof · cited by 1