OAI/Algebra/AuslanderReiten/Bar/ExternalBarFreeAugmentation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.ExternalTensor.iso_cancel_pairline 9 - def
OAI.ArExplicit.ExternalTensor.barCyclicCoverline 20 - theorem
OAI.ArExplicit.ExternalTensor.factor_augmentationline 27 - theorem
OAI.ArExplicit.ExternalTensor.barFreeCoordinate_augmentationline 36