OAI/Algebra/AuslanderReiten/Modules/TrivialInduction.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.TrivialInduction.Middle line 14
2. abbrev OAI.ArExplicit.TrivialInduction.Quotient line 15
3. instance OAI.ArExplicit.TrivialInduction.dualModule line 17
4. theorem OAI.ArExplicit.TrivialInduction.dual_smul line 20
5. instance OAI.ArExplicit.TrivialInduction.(instance at line 22) line 22
6. instance OAI.ArExplicit.TrivialInduction.(instance at line 24) line 24
7. instance OAI.ArExplicit.TrivialInduction.(instance at line 26) line 26
8. instance OAI.ArExplicit.TrivialInduction.quotientModule line 29
9. theorem OAI.ArExplicit.TrivialInduction.quotient_smul_value line 32
10. instance OAI.ArExplicit.TrivialInduction.(instance at line 35) line 35
11. instance OAI.ArExplicit.TrivialInduction.(instance at line 37) line 37
12. instance OAI.ArExplicit.TrivialInduction.(instance at line 39) line 39
13. def OAI.ArExplicit.TrivialInduction.inclusion line 42
14. def OAI.ArExplicit.TrivialInduction.projection line 57
15. theorem OAI.ArExplicit.TrivialInduction.inclusion_value line 62
16. theorem OAI.ArExplicit.TrivialInduction.projection_value line 64
17. theorem OAI.ArExplicit.TrivialInduction.inclusion_left line 67
18. theorem OAI.ArExplicit.TrivialInduction.projection_left line 76
19. theorem OAI.ArExplicit.TrivialInduction.projection_inclusion line 79
20. theorem OAI.ArExplicit.TrivialInduction.inclusion_injective line 82
21. theorem OAI.ArExplicit.TrivialInduction.projection_surjective line 86
22. theorem OAI.ArExplicit.TrivialInduction.inclusion_projection_exact line 90
23. theorem OAI.ArExplicit.TrivialInduction.dual_ideal_annihilates line 103