OAI/NumberTheory/PiExponent/LocalAlgebra/RegularSequenceExtObstruction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.W18.differentialRangeShortComplex line 20
2. theorem OAI.PiExponentJets.W18.differentialRangeShortComplex_shortExact line 28
3. def OAI.PiExponentJets.W18.augmentationRangeShortComplex line 39
4. theorem OAI.PiExponentJets.W18.augmentationRangeShortComplex_shortExact line 46
5. theorem OAI.PiExponentJets.W18.ext_subsingleton_of_subsingleton_module line 59
6. def OAI.PiExponentJets.W18.regularSequenceDifferentialRange line 72
7. theorem OAI.PiExponentJets.W18.regularSequenceDifferentialRange_top_subsingleton line 75
8. theorem OAI.PiExponentJets.W18.regular_sequence_ext_zero line 85
9. theorem OAI.PiExponentJets.W18.regular_sequence_associatedPrime_ext_obstruction line 121