OAI/Algebra/AuslanderReiten/Bar/NativeBarAugmentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ModuleBar.canonicalCoefficientAugmentation line 13
2. theorem OAI.ArExplicit.ModuleBar.coefficientScalarIso_augmentation line 19
3. theorem OAI.ArExplicit.BarBalanced.compose_augmentation line 30
4. def OAI.ArExplicit.BarBalanced.nativeEndpointObject line 40
5. def OAI.ArExplicit.BarBalanced.nativeEndpointIso line 46
6. def OAI.ArExplicit.BarBalanced.nativeEvaluatedAugmentation line 52
7. theorem OAI.ArExplicit.BarBalanced.canonicalComplexIso_augmentation line 61
8. theorem OAI.ArExplicit.BarBalanced.nativeComplexIso_augmentation line 69