OAI/Algebra/AuslanderReiten/Algebras/SimpleDual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.Resolution.simpleRightAction line 12
2. theorem OAI.ArExplicit.Resolution.simple_right_smul line 15
3. instance OAI.ArExplicit.Resolution.simpleRightModule line 18
4. instance OAI.ArExplicit.Resolution.(instance at line 39) line 39
5. def OAI.ArExplicit.Resolution.generator line 42
6. theorem OAI.ArExplicit.Resolution.generator_coordinate line 44
7. theorem OAI.ArExplicit.Resolution.simple_expand line 46
8. def OAI.ArExplicit.Resolution.rightSimpleDualEquiv line 51