OAI/Algebra/AuslanderReiten/Bar/ModuleBarAutomorphism.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ModuleBar.transport line 15
2. theorem OAI.ArExplicit.ModuleBar.transport_zero line 19
3. theorem OAI.ArExplicit.ModuleBar.transport_tmul line 20
4. theorem OAI.ArExplicit.ModuleBar.transport_left line 27
5. theorem OAI.ArExplicit.ModuleBar.transport_boundary line 38
6. def OAI.ArExplicit.ModuleBar.transportLinear line 53
7. def OAI.ArExplicit.ModuleBar.transportIso line 59
8. theorem OAI.ArExplicit.ModuleBar.transportIso_hom_apply line 64
9. def OAI.ArExplicit.ModuleBar.transportComplexIso line 69