OAI/Algebra/Finitistic/Bar/
738 declarations, 0 contain sorry, 0 declared as axioms; 93 files
Files
- Balanced.lean 20 declarations
- BalancedTensorFunctor.lean 7 declarations
- Bar.lean 25 declarations
- BarAdditive.lean 3 declarations
- BarBimoduleCongruence.lean 8 declarations
- BarCoordinateNaturality.lean 4 declarations
- BarFunctor.lean 13 declarations
- BarPatternEmbedding.lean 2 declarations
- BlockCoordinateGenerators.lean 4 declarations
- BlockIndexEquiv.lean 15 declarations
- ChainSplitting.lean 2 declarations
- CoproductHomBijections.lean 3 declarations
- CoproductHomotopy.lean 5 declarations
- CountHomologyDetection.lean 6 declarations
- CountProjective.lean 6 declarations
- CountRetracts.lean 9 declarations
- CountTorBounds.lean 3 declarations
- DerivedBarCoproduct.lean 6 declarations
- DerivedCountCoproduct.lean 1 declarations
- DerivedCountShift.lean 2 declarations
- DerivedTensorBarSplitting.lean 5 declarations
- DirectSumCoproduct.lean 5 declarations
- DirectSumExactness.lean 3 declarations
- ExplicitSignedDifferential.lean 16 declarations
- ExtensionColimits.lean 2 declarations
- FiniteBarResolution.lean 4 declarations
- FiniteSumSupport.lean 1 declarations
- FlatSupportedAssembly.lean 4 declarations
- GlobalIndexedComparison.lean 6 declarations
- IndexedAssemblyComparison.lean 8 declarations
- IndexedMultibarTotal.lean 8 declarations
- IndexedPatternEmbedding.lean 5 declarations
- InflatedParityFaces.lean 15 declarations
- IntegerCountObject.lean 2 declarations
- IntegerCountRestriction.lean 7 declarations
- IntegerCountShift.lean 6 declarations
- IntegerDerivedMultibar.lean 8 declarations
- IntegerStalk.lean 1 declarations
- KProjectiveCoproduct.lean 1 declarations
- LeadingBarSuffix.lean 15 declarations
- LeadingSuffixFaces.lean 5 declarations
- LeadingSupportedComparison.lean 12 declarations
- LeadingTotalComparison.lean 4 declarations
- LeadingTotalDifferential.lean 5 declarations
- LeadingTotalEmbedding.lean 3 declarations
- LiteralMultibarCoordinates.lean 10 declarations
- ModuleBlockIndex.lean 11 declarations
- ModuleMultibarCoordinates.lean 7 declarations
- MultibarBlocks.lean 24 declarations
- MultibarDecomposition.lean 21 declarations
- MultibarFlattenDerived.lean 7 declarations
- MultibarIndex.lean 11 declarations
- MultibarSigns.lean 13 declarations
- PatternPrefixCoordinates.lean 2 declarations
- PatternSuffixFaces.lean 5 declarations
- PatternTensorCoherence.lean 8 declarations
- Projection.lean 17 declarations
- ProjectiveTail.lean 5 declarations
- RecursiveBlockIndex.lean 9 declarations
- RecursivePrefixInclusions.lean 10 declarations
- RecursiveSuffixCoefficient.lean 6 declarations
- RecursiveSuffixDifferential.lean 5 declarations
- RecursiveSuffixEmbedding.lean 10 declarations
- RecursiveSuffixFaces.lean 12 declarations
- RecursiveSuffixInduction.lean 4 declarations
- RecursiveSuffixSums.lean 2 declarations
- RecursiveSuffixTotal.lean 9 declarations
- RecursiveTotalDifferential.lean 18 declarations
- RecursiveTotalFlatten.lean 12 declarations
- ResolutionDerived.lean 7 declarations
- SignedBlockExplicit.lean 9 declarations
- SignedBlockModel.lean 10 declarations
- SplitProjectiveTail.lean 4 declarations
- Splitting.lean 9 declarations
- StrictSupportExtension.lean 3 declarations
- SuffixNaturality.lean 8 declarations
- SuffixParityFaces.lean 12 declarations
- SupportedInnerCoordinates.lean 10 declarations
- SupportedOuterCoordinates.lean 4 declarations
- TensorModel.lean 4 declarations
- TotalAdditive.lean 4 declarations
- TotalBar.lean 10 declarations
- TotalBarComparison.lean 9 declarations
- TotalBarContraction.lean 17 declarations
- TotalBarDerived.lean 16 declarations
- TotalBarFunctor.lean 4 declarations
- TotalBarResolution.lean 6 declarations
- TotalBarTensor.lean 7 declarations
- TotalMap.lean 12 declarations
- TwoSided.lean 13 declarations
- TwoSidedBarFunctor.lean 10 declarations
- TwoSidedWeight.lean 8 declarations
- Weight.lean 9 declarations