OAI/Analysis/JiangSu/Traceless/TracelessFiniteScalarExcision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CurrentMain.Traceless.finite_scalar_cross_excision line 16
2. theorem OAI.CurrentMain.Traceless.scalar_cross_excision_ultrapower line 92
3. lemma OAI.CStarExcision.stateRowElement_mutual_cross line 151
4. lemma OAI.CStarExcision.stateRowSum_eq_sum line 165
5. theorem OAI.CurrentMain.Traceless.nuclear_cross_assembly line 187