OAI/NumberTheory/PowerFree/HilbertGrowth.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.leadingCoeff_nonneg_of_eventually_nat_eval_nonneg line 11
  2. theorem OAI.QuarticPowerFree.coeff_le_of_eventually_nat_eval_le line 24
  3. theorem OAI.QuarticPowerFree.natDegree_le_of_eventually_nat_eval_bounds line 38
  4. def OAI.QuarticPowerFree.FreeNormalFace line 58
  5. theorem OAI.QuarticPowerFree.normal_of_free_face line 61
  6. theorem OAI.QuarticPowerFree.large_coordinates_free line 73
  7. theorem OAI.QuarticPowerFree.free_face_algebraicIndependent line 86
  8. def OAI.QuarticPowerFree.partialCoordinateBox line 116
  9. theorem OAI.QuarticPowerFree.card_partialCoordinateBox_le line 121
  10. theorem OAI.QuarticPowerFree.normalExponents_card_growth line 139
  11. theorem OAI.QuarticPowerFree.totalSpace_finite line 183
  12. theorem OAI.QuarticPowerFree.totalSpace_finrank line 192
  13. theorem OAI.QuarticPowerFree.independent_coordinates_hilbert_lower line 200
  14. theorem OAI.QuarticPowerFree.empty_free_face_of_proper line 228
  15. theorem OAI.QuarticPowerFree.coordinate_hilbert_degree_independent line 242
  16. theorem OAI.QuarticPowerFree.projection_hilbert_le line 321
  17. theorem OAI.QuarticPowerFree.not_independent_over_hilbert_degree line 347
  18. theorem OAI.QuarticPowerFree.projection_equation_degree_bound line 372
  19. theorem OAI.QuarticPowerFree.exists_irreducible_in_kernel line 396
  20. theorem OAI.QuarticPowerFree.principal_coordinate_kernel line 409
  21. theorem OAI.QuarticPowerFree.principal_projection_relation line 448
  22. theorem OAI.QuarticPowerFree.quotient_aeval_rename line 507
  23. theorem OAI.QuarticPowerFree.exists_principal_relation_of_dependent line 514
  24. theorem OAI.QuarticPowerFree.prime_projection_relation line 540
  25. theorem OAI.QuarticPowerFree.prime_projection_map line 565
  26. theorem OAI.QuarticPowerFree.bounded_projection_relation line 588