Theorems · Definition · functional analysis
PositiveLinearMap.GNS
{A : Type u_1} →
[inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (A →ₚ[ℂ] ℂ) → [StarOrderedRing A] → Type u_1The Hilbert space constructed from a positive linear functional on a C⋆-algebra.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 317 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Complexstatement and proof · cited by 5,565
- StarOrderedRingstatement and proof · cited by 587
- UniformSpace.Completionproof · cited by 192
- NonUnitalCStarAlgebrastatement and proof · cited by 149
- Complex.partialOrderstatement · cited by 64
- PositiveLinearMapstatement and proof · cited by 52
- PositiveLinearMap.PreGNSproof · cited by 10
Cited by5
Results whose statement or proof uses this declaration.
- PositiveLinearMap.gnsNonUnitalStarAlgHomstatement · cited by 3
- PositiveLinearMap.gnsStarAlgHomstatement and proof · cited by 1
- PositiveLinearMap.gnsNonUnitalStarAlgHom_applystatement · cited by 0
- PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coestatement · cited by 0
- PositiveLinearMap.gnsStarAlgHom_applystatement · cited by 0