OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientHomogeneity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_real_smul line 15
2. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyValue_real_smul line 20
3. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_real_smul line 29
4. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_real_smul_re line 37