OAI/NumberTheory/PiExponent/LocalAlgebra/FreeResolutionAssociatedHeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W18.ext_subsingleton_of_shortExact line 20
2. theorem OAI.PiExponentJets.W18.ext_zero_of_finite_exact_resolution line 34
3. theorem OAI.PiExponentJets.W18.nonzero_ext_forces_resolution_obstruction line 48
4. theorem OAI.PiExponentJets.W18.lengthTwo_ext_zero line 60
5. theorem OAI.PiExponentJets.W18.associatedPrime_nonzero_quotient_hom line 77
6. theorem OAI.PiExponentJets.W18.associatedPrime_nonzero_ext_zero line 88
7. theorem OAI.PiExponentJets.W18.not_isAssociatedPrime_of_ext_zero line 97
8. theorem OAI.PiExponentJets.W18.associatedPrime_local_nonzero_ext_zero line 104