OAI/Algebra/AuslanderReiten/Bar/BarBalancedCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.BarBalanced.differential line 16
2. theorem OAI.ArExplicit.BarBalanced.differential_tmul line 22
3. theorem OAI.ArExplicit.BarBalanced.equiv_differential line 28
4. def OAI.ArExplicit.BarBalanced.cubic line 38
5. theorem OAI.ArExplicit.BarBalanced.cubic_tmul line 45
6. theorem OAI.ArExplicit.BarBalanced.equiv_cubic line 52
7. def OAI.ArExplicit.BarBalanced.complex line 65
8. theorem OAI.ArExplicit.BarBalanced.complex_d line 79
9. def OAI.ArExplicit.BarBalanced.complexIso line 84