OAI/NumberTheory/PiExponent/LocalAlgebra/FiniteFreeResolutionExt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSiegelAux.W31.projectiveResolutionOfExact line 19
2. theorem OAI.PiExponentSiegelAux.W31.projectiveResolutionOfExact_complex line 39
3. def OAI.PiExponentSiegelAux.W31.resolutionExtAddEquiv line 48
4. theorem OAI.PiExponentSiegelAux.W31.ext_subsingleton_iff_cocycles_are_boundaries line 54
5. theorem OAI.PiExponentSiegelAux.W31.ext_subsingleton_of_isZero_resolution_term line 70
6. theorem OAI.PiExponentSiegelAux.W31.module_exactAt_succ_of_range_eq_ker line 84
7. def OAI.PiExponentSiegelAux.W31.finiteFreeResolutionOfExact line 92
8. def OAI.PiExponentSiegelAux.W31.moduleFreeResolutionOfExact line 106