OAI/Analysis/Pureness/States/QuotientMatrixCornerLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.matrixCornerTerm line 11
2. lemma OAI.CuntzPureness.matrixCornerTerm_add line 13
3. lemma OAI.CuntzPureness.matrixCornerTerm_star line 17
4. lemma OAI.CuntzPureness.matrixCornerTerm_mul line 25
5. def OAI.CuntzPureness.matrixCornerLift line 39
6. lemma OAI.CuntzPureness.matrixCornerLift_single line 59
7. lemma OAI.CuntzPureness.matrixCornerLift_first line 65