OAI/Analysis/Commutator/CpCompression.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Kadison.CpCompression.compressionline 22 - lemma
OAI.Kadison.CpCompression.compression_applyline 62
OAI/Analysis/Commutator/CpCompression.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Kadison.CpCompression.compression line 22OAI.Kadison.CpCompression.compression_apply line 62