OAI/Analysis/JiangSu/Nonunital/
295 declarations, 0 contain sorry, 0 declared as axioms; 34 files
Files
- ClosedIdealBasic.lean 36 declarations
- CommonMinorant.lean 11 declarations
- CompactTraceBase.lean 10 declarations
- ControlledComparison.lean 16 declarations
- CuntzAlmostUnperforation.lean 4 declarations
- Essentiality.lean 5 declarations
- EventualFullness.lean 4 declarations
- FiniteTraceIdeal.lean 14 declarations
- Hereditary.lean 15 declarations
- IdealDensity.lean 13 declarations
- IsometricHomLimit.lean 3 declarations
- KernelCutoff.lean 1 declarations
- LimitTraceRestriction.lean 4 declarations
- MatrixComparison.lean 14 declarations
- MatrixDiagonal.lean 17 declarations
- NonUnitalHereditaryBridge.lean 4 declarations
- NonUnitalRoots.lean 7 declarations
- NormMaps.lean 7 declarations
- ProjectionGapUltrapower.lean 1 declarations
- ProjectionStrictComparison.lean 2 declarations
- PropertySI.lean 2 declarations
- QuasitraceNonUnitalRestriction.lean 4 declarations
- QuotientSurjective.lean 11 declarations
- RankIdentification.lean 19 declarations
- RationalTerms.lean 5 declarations
- Regularization.lean 4 declarations
- RelativeCoefficient.lean 8 declarations
- RelativeCommutation.lean 8 declarations
- SIRepresentatives.lean 3 declarations
- ScalarStrictComparison.lean 3 declarations
- Stabilization.lean 12 declarations
- TraceRays.lean 20 declarations
- TracialState.lean 4 declarations
- UniformGamma.lean 4 declarations