OAI/Algebra/AuslanderReiten/Bar/
476 declarations, 0 contain sorry, 0 declared as axioms; 77 files
Files
- AugmentedBarEvaluation.lean 3 declarations
- BarBalancedCanonical.lean 21 declarations
- BarBalancedCompatibility.lean 9 declarations
- BarBalancedEquiv.lean 8 declarations
- BarBalancedModule.lean 17 declarations
- BarBalancedRaw.lean 6 declarations
- BarBalancedSuffix.lean 2 declarations
- BarBimodule.lean 11 declarations
- BarCasimir.lean 11 declarations
- BarCochain.lean 16 declarations
- BarComplex.lean 21 declarations
- BarProjective.lean 8 declarations
- BarResolution.lean 5 declarations
- BarScalarCoordinates.lean 1 declarations
- BarSuffix.lean 9 declarations
- BarTensorRegular.lean 4 declarations
- BarTensorRegularCoordinates.lean 1 declarations
- BarTensorRegularIsoCoordinates.lean 1 declarations
- CanonicalBarEvaluation.lean 7 declarations
- CanonicalBarPure.lean 4 declarations
- CanonicalBarSquare.lean 1 declarations
- CanonicalBarTermValues.lean 4 declarations
- ConcreteBarFreeAugmentation.lean 5 declarations
- ConcreteNativeBar.lean 12 declarations
- ExternalBarCyclicCoordinate.lean 3 declarations
- ExternalBarEvaluation.lean 7 declarations
- ExternalBarFreeAugmentation.lean 4 declarations
- ExternalBarFreeCoordinate.lean 2 declarations
- ExternalBarFreePure.lean 2 declarations
- ExternalBarTotalFree.lean 3 declarations
- ModuleBar.lean 30 declarations
- ModuleBarAutomorphism.lean 9 declarations
- ModuleBarCochain.lean 12 declarations
- ModuleBarCubic.lean 5 declarations
- ModuleBarCubicConjugate.lean 2 declarations
- ModuleBarExtTwist.lean 2 declarations
- ModuleBarFreeAugmentation.lean 3 declarations
- ModuleBarFreeCoordinate.lean 4 declarations
- ModuleBarHomTwist.lean 7 declarations
- ModuleBarNative.lean 5 declarations
- ModuleBarNativeTransport.lean 11 declarations
- ModuleBarNativeTwist.lean 3 declarations
- ModuleBarPositiveModel.lean 1 declarations
- ModuleBarScalarClass.lean 2 declarations
- ModuleBarScalarTransport.lean 5 declarations
- ModuleBarSuffix.lean 8 declarations
- ModuleBarTensorAction.lean 2 declarations
- ModuleBarTensorAugmented.lean 2 declarations
- ModuleBarTensorCentral.lean 1 declarations
- ModuleBarTensorCentralAction.lean 2 declarations
- ModuleBarTensorClass.lean 4 declarations
- ModuleBarTensorEndpoint.lean 2 declarations
- ModuleBarTensorEndpointCoordinates.lean 1 declarations
- ModuleBarTensorExact.lean 2 declarations
- ModuleBarTensorExt.lean 12 declarations
- ModuleBarTensorGeneration.lean 1 declarations
- ModuleBarTensorHom.lean 4 declarations
- ModuleBarTensorProducts.lean 2 declarations
- ModuleBarTensorTransport.lean 3 declarations
- ModuleBarTensorTwist.lean 6 declarations
- ModuleBarTwistAction.lean 2 declarations
- ModuleBarTwistCocycle.lean 4 declarations
- ModuleBarTwistExact.lean 2 declarations
- ModuleBarTwistExtAction.lean 10 declarations
- ModuleBarTwistIdentity.lean 2 declarations
- NativeBarAugmentation.lean 8 declarations
- NativeBarCompositeValues.lean 3 declarations
- NativeBarEvaluation.lean 4 declarations
- NativeBarFreeEndpoint.lean 12 declarations
- TBarHomotopies.lean 7 declarations
- TBarLift.lean 6 declarations
- TCasimir.lean 10 declarations
- TCasimirAugmentation.lean 7 declarations
- TCasimirEvaluation.lean 7 declarations
- TCasimirSquare.lean 4 declarations
- TwistedBar.lean 23 declarations
- TwistedBarTensorRegular.lean 4 declarations