OAI/Algebra/Finitistic/Ordinary/
840 declarations, 0 contain sorry, 0 declared as axioms; 129 files
Files
- OrdinaryAssociativeTensorModules.lean 16 declarations
- OrdinaryAssociativityNaturality.lean 4 declarations
- OrdinaryBalancedActions.lean 8 declarations
- OrdinaryBalancedAssociativity.lean 13 declarations
- OrdinaryBalancedCongruence.lean 1 declarations
- OrdinaryBimodule.lean 21 declarations
- OrdinaryBimoduleAssociativeTerms.lean 3 declarations
- OrdinaryBimoduleAssociativity.lean 8 declarations
- OrdinaryBimoduleAugmentation.lean 6 declarations
- OrdinaryBimoduleAugmentationQuasiIso.lean 4 declarations
- OrdinaryBimoduleCoefficientEquiv.lean 5 declarations
- OrdinaryBimoduleCoefficients.lean 11 declarations
- OrdinaryBimoduleDerivedTensor.lean 5 declarations
- OrdinaryBimoduleResolutionProjective.lean 3 declarations
- OrdinaryBimoduleTensorFunctor.lean 2 declarations
- OrdinaryBimoduleTensorTerms.lean 5 declarations
- OrdinaryBimoduleTensorTotal.lean 8 declarations
- OrdinaryBimoduleTotalAssociativity.lean 5 declarations
- OrdinaryBimoduleTotalCongruence.lean 4 declarations
- OrdinaryBimoduleTotalForget.lean 3 declarations
- OrdinaryBimoduleTotalFunctor.lean 3 declarations
- OrdinaryBimoduleTotalMaps.lean 8 declarations
- OrdinaryBlockBimodule.lean 14 declarations
- OrdinaryBlockComplexes.lean 5 declarations
- OrdinaryBlockDerived.lean 4 declarations
- OrdinaryBlockModules.lean 10 declarations
- OrdinaryBlockTensorTerms.lean 4 declarations
- OrdinaryChainAlgebra.lean 24 declarations
- OrdinaryChainDirected.lean 5 declarations
- OrdinaryChainResolution.lean 21 declarations
- OrdinaryCochain.lean 4 declarations
- OrdinaryComplexAction.lean 22 declarations
- OrdinaryComplexTensorMaps.lean 11 declarations
- OrdinaryCompression.lean 12 declarations
- OrdinaryConeCoordinates.lean 6 declarations
- OrdinaryConeQuasiIso.lean 1 declarations
- OrdinaryDerivedIterates.lean 2 declarations
- OrdinaryDerivedSquareComparison.lean 1 declarations
- OrdinaryFiniteColumnComplex.lean 8 declarations
- OrdinaryFiniteConeReindex.lean 8 declarations
- OrdinaryFiniteConeTriangular.lean 7 declarations
- OrdinaryFinitePiSupport.lean 2 declarations
- OrdinaryFiniteTotal.lean 7 declarations
- OrdinaryFiniteTotalMaps.lean 3 declarations
- OrdinaryFirstBlockTensor.lean 8 declarations
- OrdinaryFirstBlockTotal.lean 6 declarations
- OrdinaryFirstComponentExact.lean 7 declarations
- OrdinaryFirstDerivedCompatibility.lean 9 declarations
- OrdinaryFirstDerivedRetraction.lean 8 declarations
- OrdinaryFixedTensorFunctor.lean 7 declarations
- OrdinaryFreeTensor.lean 10 declarations
- OrdinaryFreeTensorExactness.lean 3 declarations
- OrdinaryFullTensorComplex.lean 7 declarations
- OrdinaryFullTensorTerms.lean 8 declarations
- OrdinaryFunctorExtension.lean 3 declarations
- OrdinaryGenuineBimoduleComparison.lean 6 declarations
- OrdinaryGlobalDimension.lean 2 declarations
- OrdinaryIntegerResolution.lean 10 declarations
- OrdinaryLeftTensorCongruence.lean 1 declarations
- OrdinaryLeftTensorMaps.lean 2 declarations
- OrdinaryMiddleTensorFunctors.lean 6 declarations
- OrdinaryOffDiagonalComplex.lean 4 declarations
- OrdinaryOffDiagonalComplexMaps.lean 3 declarations
- OrdinaryOffDiagonalForget.lean 4 declarations
- OrdinaryOffDiagonalMaps.lean 2 declarations
- OrdinaryOffDiagonalObjects.lean 4 declarations
- OrdinaryOffDiagonalProjective.lean 3 declarations
- OrdinaryOffDiagonalSingle.lean 4 declarations
- OrdinaryPairComplex.lean 11 declarations
- OrdinaryPairQuasiIso.lean 4 declarations
- OrdinaryProductComponent.lean 8 declarations
- OrdinaryProductDimension.lean 2 declarations
- OrdinaryProductOpposite.lean 4 declarations
- OrdinaryProductProjective.lean 5 declarations
- OrdinaryProductSecondDimension.lean 3 declarations
- OrdinaryProductSplitting.lean 7 declarations
- OrdinaryProjectiveTensor.lean 7 declarations
- OrdinaryResolutionComplex.lean 12 declarations
- OrdinaryResolutionExact.lean 5 declarations
- OrdinaryResolutionModels.lean 8 declarations
- OrdinaryResolutionQuasiIso.lean 11 declarations
- OrdinaryRestrictionHomology.lean 3 declarations
- OrdinaryRetainedBimodule.lean 12 declarations
- OrdinaryRetainedCongruence.lean 2 declarations
- OrdinaryRetainedRestriction.lean 4 declarations
- OrdinaryRightProjective.lean 3 declarations
- OrdinarySecondBlockTensor.lean 8 declarations
- OrdinarySecondBlockTotal.lean 6 declarations
- OrdinaryShiftDerivedTensor.lean 4 declarations
- OrdinaryShiftSign.lean 3 declarations
- OrdinarySignedExactness.lean 1 declarations
- OrdinarySimulationComparison.lean 6 declarations
- OrdinarySingleTensorTerms.lean 12 declarations
- OrdinarySingleTensorTotal.lean 6 declarations
- OrdinarySourceBimoduleTotal.lean 1 declarations
- OrdinarySourceDerivedComparison.lean 2 declarations
- OrdinarySourceResolutionModels.lean 4 declarations
- OrdinarySupportedExtension.lean 4 declarations
- OrdinaryTensorAugmentation.lean 11 declarations
- OrdinaryTensorBimap.lean 5 declarations
- OrdinaryTensorBimoduleComparison.lean 14 declarations
- OrdinaryTensorBimoduleResolution.lean 9 declarations
- OrdinaryTensorColumnAcyclic.lean 2 declarations
- OrdinaryTensorDerivedFunctor.lean 3 declarations
- OrdinaryTensorDifferential.lean 6 declarations
- OrdinaryTensorDirected.lean 10 declarations
- OrdinaryTensorExactness.lean 6 declarations
- OrdinaryTensorFiniteMatrix.lean 11 declarations
- OrdinaryTensorGlobalDimension.lean 3 declarations
- OrdinaryTensorIdeal.lean 10 declarations
- OrdinaryTensorIdealActions.lean 8 declarations
- OrdinaryTensorInputMaps.lean 7 declarations
- OrdinaryTensorMixedSign.lean 3 declarations
- OrdinaryTensorResolution.lean 10 declarations
- OrdinaryTensorResolutionComplex.lean 12 declarations
- OrdinaryTensorRightRestriction.lean 2 declarations
- OrdinaryTensorTotalAcyclic.lean 6 declarations
- OrdinaryTensorTotalFunctor.lean 6 declarations
- OrdinaryTensorTotalQuasiIso.lean 4 declarations
- OrdinaryTensorVertex.lean 4 declarations
- OrdinaryTerminal.lean 15 declarations
- OrdinaryTerminalResolution.lean 10 declarations
- OrdinaryTriangularExactness.lean 1 declarations
- OrdinaryTwoSidedTensor.lean 11 declarations
- OrdinaryVertexCompression.lean 8 declarations
- OrdinaryXAugmentation.lean 5 declarations
- OrdinaryXBlockComparison.lean 3 declarations
- OrdinaryXDerivedTensor.lean 5 declarations
- OrdinaryXResolution.lean 8 declarations