OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientCStar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotient_norm_square_le line 12
  2. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientCStarAlgebra line 53
  3. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientRealAlgebra line 57

    Source documentation

    The real scalar structure inherited from the complex Cā‹†-algebra.

    instance cauchyQuotientRealAlgebra : Algebra ā„ (T.CauchyQuotient hadd) :=
ā€¦
  4. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientRealStarModule line 60