OAI/NumberTheory/PowerFree/NormalMonomials.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.IdealNormal line 11
  2. theorem OAI.QuarticPowerFree.ideal_normal_form line 15
  3. theorem OAI.QuarticPowerFree.ideal_normal_injective line 45
  4. theorem OAI.QuarticPowerFree.ideal_normal_quotient_bijective line 51
  5. def OAI.QuarticPowerFree.idealNormalEquiv line 72
  6. def OAI.QuarticPowerFree.idealNormalBasis line 81
  7. theorem OAI.QuarticPowerFree.ideal_normal_finite_obstructions line 86
  8. def OAI.QuarticPowerFree.totalSpace line 108
  9. theorem OAI.QuarticPowerFree.mem_totalSpace line 111
  10. def OAI.QuarticPowerFree.normalTotalSpace line 116
  11. theorem OAI.QuarticPowerFree.normalTotalSpace_le line 120
  12. theorem OAI.QuarticPowerFree.totalSpace_image_normal line 125
  13. theorem OAI.QuarticPowerFree.coordinate_hilbert_count line 141
  14. def OAI.QuarticPowerFree.simplexTuple line 162
  15. theorem OAI.QuarticPowerFree.mem_simplexTuple line 165
  16. theorem OAI.QuarticPowerFree.card_antidiagonalTuple line 174
  17. theorem OAI.QuarticPowerFree.card_simplexTuple line 193
  18. def OAI.QuarticPowerFree.simplexExponents line 205
  19. theorem OAI.QuarticPowerFree.mem_simplexExponents line 208
  20. theorem OAI.QuarticPowerFree.card_simplexExponents line 216
  21. def OAI.QuarticPowerFree.normalExponents line 220
  22. theorem OAI.QuarticPowerFree.mem_normalExponents line 225
  23. theorem OAI.QuarticPowerFree.normalExponents_empty line 231
  24. def OAI.QuarticPowerFree.colonMonomials line 236
  25. theorem OAI.QuarticPowerFree.colonMonomials_card_le line 241
  26. theorem OAI.QuarticPowerFree.finsupp_tsub_le_iff line 246
  27. theorem OAI.QuarticPowerFree.normalExponents_card_insert line 253
  28. theorem OAI.QuarticPowerFree.normalExponents_eventually_polynomial line 291
  29. theorem OAI.QuarticPowerFree.coordinate_hilbert_eventually_polynomial line 338
  30. theorem OAI.QuarticPowerFree.idealNormal_span_singleton line 359
  31. theorem OAI.QuarticPowerFree.hypersurface_hilbert_count line 371
  32. theorem OAI.QuarticPowerFree.binomial_difference_sum line 391
  33. def OAI.QuarticPowerFree.hypersurfaceHilbertPolynomial line 408
  34. theorem OAI.QuarticPowerFree.hypersurfaceHilbertPolynomial_coeff line 411
  35. theorem OAI.QuarticPowerFree.hypersurfaceHilbertPolynomial_degree line 415
  36. theorem OAI.QuarticPowerFree.hypersurface_hilbert_polynomial line 421