OAI/Algebra/AuslanderReiten/Bar/BarBalancedEquiv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.BarBalanced.embedding line 13
2. theorem OAI.ArExplicit.BarBalanced.embedding_succ line 18
3. theorem OAI.ArExplicit.BarBalanced.evaluation_prepend line 22
4. theorem OAI.ArExplicit.BarBalanced.evaluation_embedding line 33
5. theorem OAI.ArExplicit.BarBalanced.embedding_rawEval line 44
6. theorem OAI.ArExplicit.BarBalanced.embedding_evaluation line 63
7. def OAI.ArExplicit.BarBalanced.equiv line 75
8. theorem OAI.ArExplicit.BarBalanced.equiv_tmul line 81