OAI/Analysis/JiangSu/CentralSequences/
291 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- ApproximateCentralMatrixSupply.lean 17 declarations
- CStarCentralWeights.lean 3 declarations
- CentralGeneralizedLargeness.lean 7 declarations
- CentralMatrix.lean 1 declarations
- CentralSaturation.lean 1 declarations
- CentralSequenceSigmaIdeal.lean 2 declarations
- CoefficientSaturation.lean 1 declarations
- CountableArraySaturation.lean 15 declarations
- FamilyFiniteCentral.lean 1 declarations
- FiniteCentral.lean 3 declarations
- IdentitySaturation.lean 1 declarations
- MatrixCompressionCentrality.lean 3 declarations
- NormCentralFunctionalCalculus.lean 6 declarations
- NormCentralSequenceAlgebra.lean 34 declarations
- NormTraceKernelSigma.lean 5 declarations
- NormUltrapowerArrayTest.lean 8 declarations
- NormUltrapowerBasic.lean 44 declarations
- NormUltrapowerEpsilonTest.lean 1 declarations
- NormUltrapowerIdentitySaturation.lean 1 declarations
- NormUltrapowerMaps.lean 11 declarations
- NormUltrapowerPositive.lean 3 declarations
- NormUltrapowerToTracial.lean 23 declarations
- NormUltrapowerUnitaryLift.lean 2 declarations
- OrderZeroContractiveCut.lean 6 declarations
- ProjectionSaturation.lean 1 declarations
- QuasicentralFinite.lean 8 declarations
- QuasicentralResolvent.lean 21 declarations
- RelativeCentralMap.lean 10 declarations
- RelativeCentralQuotient.lean 15 declarations
- SigmaOrderZeroLift.lean 2 declarations
- SmallTraceNormUltrapower.lean 3 declarations
- TracialIsometrySaturation.lean 1 declarations
- TracialMatrixModelSaturation.lean 9 declarations
- UnitalNormCentralAlgebra.lean 14 declarations
- UnitalTraceKernelSigma.lean 8 declarations