OAI/NumberTheory/SiegelZeros/Hilbert/HilbertSeries.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.PowerSeries.coeff_mul_invOneSubPow_one line 20
  2. theorem OAI.SiegelZeros.PowerSeries.sum_coeff_mul_invOneSubPow line 25
  3. theorem OAI.SiegelZeros.PowerSeries.sum_coeff_mul_invOneSubPow_eq_hilbertPoly_eval line 30
  4. theorem OAI.SiegelZeros.PowerSeries.exists_reduced_mul_invOneSubPow line 37
  5. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertSeries line 72
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertSeries_eq_add_X_mul_colon line 75
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_hilbertSeries_numerator line 89
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_hilbertSeries_eq_mul_invOneSubPow line 125
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.existsUnique_hilbertPolynomial line 131
  10. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial line 139
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_spec line 143
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_eq_of_eventual_eval line 149
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_component_cumulative_hilbertPoly line 156
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_reduced_hilbertSeries line 170
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_cumulative_hilbertPolynomial line 179
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.leadingCoeff_pos_of_eventually_nat_eval_nonneg line 221
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.numerator_eval_one_is_integer line 243
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.exists_pos_integer_factorial_mul_leadingCoeff_hilbertPolynomial line 272
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree line 324
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_cast line 329
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_pos_iff line 343
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_eq_zero_iff line 354
  23. theorem OAI.SiegelZeros.WeightedTorusJets.decompose_smul_of_homogeneous_right line 375
  24. theorem OAI.SiegelZeros.WeightedTorusJets.homogeneous_component_smul_mem line 393
  25. theorem OAI.SiegelZeros.WeightedTorusJets.exists_homogeneous_annihilator_of_annihilator line 404
  26. theorem OAI.SiegelZeros.WeightedTorusJets.exists_homogeneous_annihilator_of_rank_zero line 418
  27. theorem OAI.SiegelZeros.WeightedTorusJets.decompose_smul_mem_of_homogeneous line 435
  28. theorem OAI.SiegelZeros.WeightedTorusJets.homogeneous_submodule_span line 456
  29. theorem OAI.SiegelZeros.WeightedTorusJets.homogeneous_coefficients_sum_mem line 473
  30. theorem OAI.SiegelZeros.WeightedTorusJets.exists_homogeneous_coefficients line 488