OAI/Analysis/KadisonSimilarity/Derivation/
354 declarations, 0 contain sorry, 0 declared as axioms; 42 files
Files
- BoundedHomRestriction.lean 4 declarations
- BoundedHomRow.lean 4 declarations
- CStarRowSquare.lean 2 declarations
- ColumnCompression.lean 3 declarations
- CommonCyclicEmbedding.lean 12 declarations
- CommonCyclicIntertwining.lean 2 declarations
- CountableCyclicDecomposition.lean 1 declarations
- CyclicApproximation.lean 10 declarations
- CyclicColumnPolar.lean 7 declarations
- CyclicColumnTests.lean 12 declarations
- CyclicCommutativeModel.lean 7 declarations
- CyclicDecomposition.lean 26 declarations
- CyclicDerivations.lean 10 declarations
- CyclicFactorization.lean 18 declarations
- CyclicGraphEmbedding.lean 5 declarations
- CyclicGraphSequences.lean 2 declarations
- CyclicSpectralIsometry.lean 8 declarations
- CyclicSpectralSum.lean 5 declarations
- CyclicStandardEmbedding.lean 3 declarations
- CyclicSummandColumns.lean 16 declarations
- DerivationDefectSpace.lean 6 declarations
- DerivationEndgame.lean 2 declarations
- Derivations.lean 12 declarations
- DiagonalMatrixNorm.lean 6 declarations
- DicksonAdjoint.lean 6 declarations
- DicksonDischarge.lean 1 declarations
- DicksonRow.lean 8 declarations
- FactorizationGeometry.lean 3 declarations
- FactorizationSpace.lean 4 declarations
- FinalDerivations.lean 7 declarations
- FiniteDerivationColumns.lean 5 declarations
- GrothendieckMatrix.lean 25 declarations
- GrothendieckUltrapower.lean 16 declarations
- HomPolarBound.lean 2 declarations
- Main.lean 13 imports, no declarations
- NormAttainingGrothendieck.lean 11 declarations
- NormalCyclicGraph.lean 1 declarations
- OrbitSquareNormalization.lean 3 declarations
- QuadraticSandwich.lean 11 declarations
- RectangularDerivations.lean 36 declarations
- SharpDerivationImplementation.lean 1 declarations
- TracialCornerCyclicity.lean 31 declarations