OAI/Algebra/AuslanderReiten/Resolutions/TrivialInductionQuotient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.TrivialInduction.inflate line 15
2. instance OAI.ArExplicit.TrivialInduction.(instance at line 18) line 18
3. instance OAI.ArExplicit.TrivialInduction.baseComm line 21
4. def OAI.ArExplicit.TrivialInduction.quotientScalarMap line 26
5. theorem OAI.ArExplicit.TrivialInduction.quotientScalarMap_tmul line 33
6. def OAI.ArExplicit.TrivialInduction.quotientEquiv line 37
7. def OAI.ArExplicit.TrivialInduction.quotientFunctorIso line 61
8. def OAI.ArExplicit.TrivialInduction.quotientComplexIso line 71
9. instance OAI.ArExplicit.TrivialInduction.(instance at line 76) line 76