OAI/Analysis/JiangSu/DimensionDrop/DimensionDropSurgeryEstimates.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.JiangSuConstruction.rightUnitary_conjugationline 17 - lemma
OAI.JiangSuConstruction.pFlow_commute_drop_oneline 24 - lemma
OAI.JiangSuConstruction.qFlow_commute_drop_zeroline 31 - lemma
OAI.JiangSuConstruction.surgerySection_controlline 39