OAI/Analysis/Unitarizability/NearOne.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Dixmier.nonamenable_near_oneline 13 - theorem
OAI.Dixmier.nonamenable_near_one_largeline 87
OAI/Analysis/Unitarizability/NearOne.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Dixmier.nonamenable_near_one line 13OAI.Dixmier.nonamenable_near_one_large line 87