OAI/Algebra/AuslanderReiten/Resolutions/TrivialInductionComplex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.TrivialInduction.dualComplex line 17
2. def OAI.ArExplicit.TrivialInduction.inducedComplex line 21
3. def OAI.ArExplicit.TrivialInduction.quotientComplex line 25
4. def OAI.ArExplicit.TrivialInduction.sequence line 29
5. theorem OAI.ArExplicit.TrivialInduction.sequence_shortExact line 34
6. instance OAI.ArExplicit.TrivialInduction.induced_term_projective line 41
7. instance OAI.ArExplicit.TrivialInduction.induced_term_finite line 46
8. theorem OAI.ArExplicit.TrivialInduction.dualComplex_ideal_zero line 51
9. def OAI.ArExplicit.TrivialInduction.triangle line 67
10. theorem OAI.ArExplicit.TrivialInduction.triangle_distinguished line 70