OAI/NumberTheory/PiExponent/LocalAlgebra/CumulativeHilbertSections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W25.restrictTotalDegree_eq_iSup_homogeneous line 17
2. theorem OAI.PiExponentJets.W25.quotientDegreeFiltration_eq_iSup_sections line 39
3. theorem OAI.PiExponentJets.W25.cumulativeSectionMap_injective line 46
4. theorem OAI.PiExponentJets.W25.cumulativeSectionMap_range line 52
5. def OAI.PiExponentJets.W25.cumulativeHomogeneousQuotientEquiv line 58
6. theorem OAI.PiExponentJets.W25.cumulativeHomogeneousQuotientEquiv_apply line 67
7. theorem OAI.PiExponentJets.W25.quotientDegreeFiltration_finrank_eq_sum_fin line 76
8. theorem OAI.PiExponentJets.W25.quotientDegreeFiltration_finrank_eq_sum line 84