OAI/NumberTheory/PiExponent/LocalAlgebra/RegularCutHistory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponentJets.W22.HomogeneousPolynomialIdeal line 13
2. def OAI.PiExponentJets.W22.zeroHomogeneousIdeal line 16
3. structure OAI.PiExponentJets.W22.RegularPrefixCut line 19
4. def OAI.PiExponentJets.W22.RegularPrefixCut.next line 44
5. theorem OAI.PiExponentJets.W22.RegularPrefixCut.degree_step line 47
6. inductive OAI.PiExponentJets.W22.ActualRegularCutHistory line 56
7. theorem OAI.PiExponentJets.W22.ActualRegularCutHistory.degree_bound line 65
8. theorem OAI.PiExponentJets.W22.actualMultiplicityCycle_zero_degree line 82
9. theorem OAI.PiExponentJets.W22.ActualRegularCutHistory.local_length_bound line 122