OAI/LinearAlgebra/CirculantHadamard/
854 declarations, 0 contain sorry, 0 declared as axioms; 68 files
Files
- AlternatingField.lean 3 declarations
- AlternatingLocalization.lean 30 declarations
- AlternatingNorm.lean 2 declarations
- AlternatingProducts.lean 28 declarations
- AlternatingTorsion.lean 5 declarations
- Basic.lean 4 declarations
- BinaryBlocks.lean 30 declarations
- BinaryCharacterSum.lean 21 declarations
- BinaryCoefficients.lean 45 declarations
- BinaryContradiction.lean 2 declarations
- BinaryEvaluation.lean 35 declarations
- BinaryLocalFamily.lean 3 declarations
- BinaryLocalRing.lean 23 declarations
- BinaryLocalization.lean 6 declarations
- BinaryNorms.lean 16 declarations
- BinaryProductTransport.lean 8 declarations
- BinaryResidue.lean 11 declarations
- CoefficientEvaluation.lean 6 declarations
- CyclicEvaluation.lean 13 declarations
- CyclicEvaluationAt.lean 11 declarations
- CyclicEvaluationProjection.lean 1 declarations
- CyclicNorm.lean 17 declarations
- CyclicPolynomial.lean 23 declarations
- CyclicProjection.lean 13 declarations
- CyclicProjectionPolynomial.lean 3 declarations
- CyclicRing.lean 39 declarations
- CyclicScalarDivision.lean 8 declarations
- CyclotomicAdjoin.lean 12 declarations
- CyclotomicAwayLocal.lean 14 declarations
- CyclotomicFactorDivision.lean 1 declarations
- CyclotomicIntegerEvaluation.lean 6 declarations
- CyclotomicLocalBase.lean 21 declarations
- CyclotomicProjection.lean 9 declarations
- CyclotomicRemainder.lean 8 declarations
- CyclotomicRings.lean 64 declarations
- CyclotomicTorsion.lean 1 declarations
- DyadicRemainder.lean 16 declarations
- FirstOrderResidue.lean 9 declarations
- IntegerLocalDivisibility.lean 2 declarations
- IntegerTwoLocal.lean 16 declarations
- Kronecker.lean 2 declarations
- LocalComparison.lean 9 declarations
- LocalComparisonInduction.lean 5 declarations
- LocalDVR.lean 7 declarations
- LocalizationIntersection.lean 3 declarations
- LocalizationMaps.lean 8 declarations
- Main.lean 1 declarations
- MatrixBridge.lean 10 declarations
- ModEight.lean 7 declarations
- Model.lean 5 declarations
- OrderCyclotomicDivisibility.lean 2 declarations
- OrderDescent.lean 2 declarations
- OrderHalving.lean 14 declarations
- OrderProjection.lean 4 declarations
- OrderReduction.lean 2 declarations
- OrderSquareEven.lean 5 declarations
- PrimeCharacterEvaluations.lean 50 declarations
- PrimeComponents.lean 36 declarations
- ProjectionCoefficients.lean 5 declarations
- ProjectionPairFiber.lean 2 declarations
- RamifiedConjugation.lean 16 declarations
- RamifiedEisenstein.lean 13 declarations
- RamifiedLocal.lean 17 declarations
- RamifiedUnit.lean 2 declarations
- ResidueOneAssociation.lean 15 declarations
- ResidueTorsion.lean 5 declarations
- TwoAdicDecomposition.lean 3 declarations
- Witnesses.lean 19 declarations