OAI/NumberTheory/PiExponent/LocalAlgebra/PrimeCutBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.W22.actualLocalLength line 15
2. theorem OAI.PiExponentJets.W22.actualLocalLength_spec line 20
3. theorem OAI.PiExponentJets.W22.primeCut_isHomogeneous line 38
4. theorem OAI.PiExponentJets.W22.actualHP_prime_cut_degree_multiplicity line 51
5. theorem OAI.PiExponentJets.W22.prime_cut_component_budget line 71
6. theorem OAI.PiExponentJets.W22.actualHP_natDegree_of_prime_dimension line 98