OAI/NumberTheory/SiegelZeros/Hilbert/HilbertMultiplicityFiltration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W22.polynomial_eq_of_nat_tail line 17
  2. def OAI.SiegelZeros.WeightedTorusJets.W22.actualHP line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_eventually line 33
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_unique line 39
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_congr line 50
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_top line 57
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_leadingCoeff_nonneg line 66
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_natDegree_antitone line 75
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_colon_step line 94
  10. def OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicity line 120
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicity_congr line 124
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicity_nonneg line 131
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicity_top line 138
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicity_cyclic_step line 144
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W22.rational_filtration_telescope line 163