OAI/Algebra/AuslanderReiten/Modules/CoinducedBimodule.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.Coinduced.(instance at line 8) line 8
2. theorem OAI.ArExplicit.Coinduced.functional_right line 13
3. instance OAI.ArExplicit.Coinduced.(instance at line 16) line 16
4. instance OAI.ArExplicit.Coinduced.(instance at line 24) line 24
5. instance OAI.ArExplicit.Coinduced.(instance at line 26) line 26
6. instance OAI.ArExplicit.Coinduced.(instance at line 28) line 28