OAI/NumberTheory/SiegelZeros/Hilbert/HilbertZeroVariables.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W64.homogeneous_mem_step_decomposition line 27
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W64.homogeneous_mem_step_of_degree_lt line 55
  3. def OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionFactor line 86
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionFactor_surjective line 98
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionFactor_ker_eq line 108
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_hilbert_step line 150
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbert_step_of_degree_lt line 165
  8. def OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries line 205
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W64.coeff_sectionHilbertSeries line 209
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_regular_step line 214
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W64.ideal_le_colon_singleton line 245
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionFactor_colon_ker line 252
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionMultiply_range_finrank_colon line 269
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W64.colon_hilbert_step line 286
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_colon_step line 300
  16. def OAI.SiegelZeros.WeightedTorusJets.W64.exponentDegreeEquivSym line 327
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W64.card_exponents_degree line 342
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSection_bot_finrank line 351
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSection_bot_finrank_multichoose line 359
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_bot line 364
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSection_finrank_zero_of_no_variables line 386
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_no_variables line 395
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W64.exists_hilbert_numerator_no_variables line 405