OAI/NumberTheory/SiegelZeros/Hilbert/ProperHypersurfaceHilbert.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W27.difference_taylor_coefficient line 20
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W27.difference_taylor_natDegree_le line 37
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W27.backward_difference_degree_and_leading line 50
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W27.backward_difference_multiplicity line 70
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W27.backward_difference_eq_comp line 81
  6. def OAI.SiegelZeros.WeightedTorusJets.W64.colonHilbertNumerator line 97
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W64.stabilized_colon_polynomial_numerator line 101
  8. def OAI.SiegelZeros.WeightedTorusJets.W64.degreePolynomial line 150
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W64.degreePolynomial_eval_one line 153
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_series_polynomial line 159
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_section_dimension_coeff line 180
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_section_dimension_eq_zero line 192
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_section_dimension_sum line 206
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_section_dimension_sum_le line 230
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W64.iteratedColon_eq_colon_power line 260
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_rename line 267
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W64.sectionHilbertSeries_coordinate line 275
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W64.exists_homogeneous_hilbert_numerator line 283
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_series_general line 350
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W64.degreePolynomial_coe line 362
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_series_residual line 378
  22. def OAI.SiegelZeros.WeightedTorusJets.W64.rationalSectionHilbertSeries line 395
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W64.coeff_rationalSectionHilbertSeries line 399
  24. def OAI.SiegelZeros.WeightedTorusJets.W64.rationalDegreePolynomial line 405
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W64.rationalDegreePolynomial_eval_one line 408
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W64.map_int_invOneSubPow line 414
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W64.rational_regular_sequence_series_residual line 425
  28. def OAI.SiegelZeros.WeightedTorusJets.W64.regularSequenceHilbertPolynomial line 440
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regularSequenceHilbertPolynomial_eventually_exact line 445
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbertPolynomial_top_coefficient line 458
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbertPolynomial_natDegree_le line 469
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbertPolynomial_degree_and_leading line 478
  33. def OAI.SiegelZeros.WeightedTorusJets.W64.hilbertMultiplicity line 492
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regularSequenceHilbertPolynomial_multiplicity line 495
  35. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_has_hilbert_polynomial_with_degree_product line 508
  36. def OAI.SiegelZeros.WeightedTorusJets.W64.shiftHilbertPolynomial line 536
  37. theorem OAI.SiegelZeros.WeightedTorusJets.W64.shiftHilbertPolynomial_eval line 539
  38. theorem OAI.SiegelZeros.WeightedTorusJets.W64.shiftHilbertPolynomial_natDegree line 544
  39. theorem OAI.SiegelZeros.WeightedTorusJets.W64.shiftHilbertPolynomial_leadingCoeff line 549
  40. theorem OAI.SiegelZeros.WeightedTorusJets.W64.shiftHilbertPolynomial_top_coeff line 556
  41. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbertMultiplicity_shift line 573
  42. theorem OAI.SiegelZeros.WeightedTorusJets.W64.hilbertMultiplicity_add line 579
  43. theorem OAI.SiegelZeros.WeightedTorusJets.W64.colon_hilbert_polynomial_eventually line 583
  44. theorem OAI.SiegelZeros.WeightedTorusJets.W64.colon_hilbert_polynomial_multiplicity line 608
  45. theorem OAI.SiegelZeros.WeightedTorusJets.W64.rational_hilbert_numerator line 626
  46. theorem OAI.SiegelZeros.WeightedTorusJets.W64.exists_homogeneous_hilbert_polynomial line 636
  47. theorem OAI.SiegelZeros.WeightedTorusJets.W64.exists_homogeneous_hilbert_polynomial_degree_le line 648
  48. theorem OAI.SiegelZeros.WeightedTorusJets.W64.prime_quotient_right_regular line 676
  49. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_hypersurface_polynomial_eventually line 685
  50. theorem OAI.SiegelZeros.WeightedTorusJets.W64.prime_hypersurface_actual_hilbert_degree line 710