OAI/Analysis/Quantum/PPTSquare/
1760 declarations, 0 contain sorry, 0 declared as axioms; 61 files
Files
- AffineMinors.lean 16 declarations
- AlgebraData.lean 13 declarations
- ChannelCompletion.lean 12 declarations
- ChannelModel.lean 38 declarations
- Commutators.lean 63 declarations
- Compression.lean 24 declarations
- Directions.lean 7 declarations
- EigenGalois.lean 2 declarations
- EigenRows.lean 5 declarations
- Evaluation.lean 8 declarations
- ExplicitMaps.lean 14 declarations
- FieldExtension.lean 5 declarations
- GaloisAction.lean 20 declarations
- InfinityMinors.lean 17 declarations
- MatrixInverse.lean 32 declarations
- MatrixSelection.lean 4 declarations
- Mod131Data.lean 6 declarations
- Mod131Powers01.lean 64 declarations
- Mod131Powers02.lean 64 declarations
- Mod131Powers03.lean 64 declarations
- Mod131Powers04.lean 53 declarations
- Mod131Products.lean 46 declarations
- Mod131Reduction.lean 43 declarations
- Mod131Result.lean 7 imports, no declarations
- Mod139Data.lean 6 declarations
- Mod139Powers01.lean 64 declarations
- Mod139Powers02.lean 64 declarations
- Mod139Powers03.lean 64 declarations
- Mod139Powers04.lean 64 declarations
- Mod139Powers05.lean 30 declarations
- Mod139Products.lean 46 declarations
- Mod139Reduction.lean 43 declarations
- Mod139Result.lean 8 imports, no declarations
- Mod41Data.lean 6 declarations
- Mod41Powers01.lean 64 declarations
- Mod41Powers02.lean 64 declarations
- Mod41Powers03.lean 64 declarations
- Mod41Powers04.lean 64 declarations
- Mod41Powers05.lean 64 declarations
- Mod41Powers06.lean 41 declarations
- Mod41Products.lean 46 declarations
- Mod41Reduction.lean 43 declarations
- Mod41Result.lean 9 imports, no declarations
- Modular.lean 4 imports, no declarations
- ModularSupport.lean 32 declarations
- Multiplication.lean 65 declarations
- OrderedChannel.lean 14 declarations
- PairResult.lean 9 declarations
- PencilData.lean 5 declarations
- PencilGeometry.lean 15 declarations
- PencilPoints.lean 7 declarations
- QuadraticBasis.lean 9 declarations
- QuadraticCriterion.lean 18 declarations
- QuadraticEvaluation.lean 2 declarations
- Recurrence.lean 13 declarations
- SplittingField.lean 13 declarations
- SplittingSetup.lean 4 declarations
- SymmetricVectors.lean 24 declarations
- TensorModel.lean 35 declarations
- TensorPositivity.lean 26 declarations
- TraceCompletion.lean 12 declarations