OAI/Analysis/Pureness/States/FiniteQuasitraceCStarValue.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteQuasitraceCStarAlgebra line 19
2. lemma OAI.CuntzPureness.finiteQuasitraceCauchyValue_continuous line 21
3. lemma OAI.CuntzPureness.finiteQuasitraceCauchyValue_square_eq_zero_iff line 25
4. lemma OAI.CuntzPureness.finiteQuasitraceCauchyValue_cfc_add line 30
5. lemma OAI.CuntzPureness.finiteQuasitraceCauchyQuotient_finite line 38
6. lemma OAI.CuntzPureness.finiteQuasitraceCStarValue_internal_root_rank line 43