OAI/Algebra/AuslanderReiten/Modules/TInducedHom.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.tInducedCochain line 15
2. theorem OAI.ArExplicit.Resolution.inducedE_hom_zero line 19
3. theorem OAI.ArExplicit.Resolution.tInduced_term_hom_zero line 25
4. theorem OAI.ArExplicit.Resolution.tInducedCochain_term_hom_zero line 35
5. theorem OAI.ArExplicit.Resolution.tInduced_fullCochain_zero line 49
6. instance OAI.ArExplicit.Resolution.tInducedCochain_kprojective line 56