`OAI/Analysis/JiangSu/Traces/`

49 declarations, 0 contain sorry, 0 declared as axioms; 8 files

Files

CompletedSharedTrace.lean 3 declarations
FaithfulTrace.lean 9 declarations
NormAnnihilatorTraceKernel.lean 3 declarations
SmallTracePeakIsometry.lean 2 declarations
SmallTraceTransfer.lean 2 declarations
TraceAlgebra.lean 25 declarations
TraceRankApproximation.lean 1 declarations
UnitalNormToTracial.lean 4 declarations