OAI/Analysis/JiangSu/Nonunital/QuasitraceNonUnitalRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.PositiveQuasitrace.nonUnitalSubalgebraSelfAdjointMap line 16
2. def OAI.Pureness.PositiveQuasitrace.nonUnitalSubalgebraRealLinear line 21
3. def OAI.Pureness.PositiveQuasitrace.nonUnitalSubalgebraComplexLinear line 30
4. lemma OAI.Pureness.PositiveQuasitrace.nonUnitalSubalgebraComplexLinear_eq line 38