OAI/Algebra/AuslanderReiten/Bar/ConcreteBarFreeAugmentation.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.T.coordinate_generatorline 16 - theorem
OAI.ArExplicit.T.tensorCyclicCover_eq_augmentationline 23 - theorem
OAI.ArExplicit.T.barCyclicCover_eq_augmentationline 36 - def
OAI.ArExplicit.T.simpleBarFreeCoordinateline 47 - theorem
OAI.ArExplicit.T.simpleBarFreeCoordinate_augmentationline 52