OAI/NumberTheory/Jacobsthal/Siegel/HilbertSeries.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.PowerSeries.coeff_mul_invOneSubPow_one line 23
  2. theorem OAI.Erdos970.PowerSeries.sum_coeff_mul_invOneSubPow line 28
  3. theorem OAI.Erdos970.PowerSeries.sum_coeff_mul_invOneSubPow_eq_hilbertPoly_eval line 33
  4. theorem OAI.Erdos970.PowerSeries.exists_reduced_mul_invOneSubPow line 40
  5. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertSeries line 75
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertSeries_eq_add_X_mul_colon line 78
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_hilbertSeries_numerator line 92
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_hilbertSeries_eq_mul_invOneSubPow line 128
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.existsUnique_hilbertPolynomial line 134
  10. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial line 142
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_spec line 146
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_eq_of_eventual_eval line 152
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_component_cumulative_hilbertPoly line 159
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_reduced_hilbertSeries line 173
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_cumulative_hilbertPolynomial line 182
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.leadingCoeff_pos_of_eventually_nat_eval_nonneg line 224
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.numerator_eval_one_is_integer line 246
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.exists_pos_integer_factorial_mul_leadingCoeff_hilbertPolynomial line 275
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree line 327
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_cast line 332
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_pos_iff line 346
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_eq_zero_iff line 357
  23. theorem OAI.Erdos970.WeightedTorusJets.decompose_smul_of_homogeneous_right line 379
  24. theorem OAI.Erdos970.WeightedTorusJets.homogeneous_component_smul_mem line 397
  25. theorem OAI.Erdos970.WeightedTorusJets.exists_homogeneous_annihilator_of_annihilator line 408
  26. theorem OAI.Erdos970.WeightedTorusJets.exists_homogeneous_annihilator_of_rank_zero line 422
  27. theorem OAI.Erdos970.WeightedTorusJets.decompose_smul_mem_of_homogeneous line 439
  28. theorem OAI.Erdos970.WeightedTorusJets.homogeneous_submodule_span line 460
  29. theorem OAI.Erdos970.WeightedTorusJets.homogeneous_coefficients_sum_mem line 477
  30. theorem OAI.Erdos970.WeightedTorusJets.exists_homogeneous_coefficients line 492