OAI/NumberTheory/SiegelZeros/LocalAlgebra/RegularCutHistory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SiegelZeros.WeightedTorusJets.W22.HomogeneousPolynomialIdeal line 17
2. def OAI.SiegelZeros.WeightedTorusJets.W22.zeroHomogeneousIdeal line 20
3. structure OAI.SiegelZeros.WeightedTorusJets.W22.RegularPrefixCut line 23
4. def OAI.SiegelZeros.WeightedTorusJets.W22.RegularPrefixCut.next line 48
5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RegularPrefixCut.degree_step line 51
6. inductive OAI.SiegelZeros.WeightedTorusJets.W22.ActualRegularCutHistory line 60
7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.ActualRegularCutHistory.degree_bound line 69
8. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle_zero_degree line 86
9. theorem OAI.SiegelZeros.WeightedTorusJets.W22.ActualRegularCutHistory.local_length_bound line 126