OAI/Analysis/JiangSu/Excision/FiniteNuclearIdentityExcision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectComparison.finite_nuclear_identity_excision line 22
2. lemma OAI.CStarExcision.commutator_square_identity line 67
3. theorem OAI.CStarExcision.commutator_sq_le line 74
4. theorem OAI.CStarExcision.commutator_le_of_excision_errors line 98
5. theorem OAI.CStarExcision.commute_of_excision line 119