OAI/NumberTheory/PowerFree/ResidueRelations.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.physicalBranchAllowance line 18
  2. theorem OAI.QuarticPowerFree.physical_forest_count line 25
  3. theorem OAI.QuarticPowerFree.pow_sum_dvd_det_of_row_dvd line 81
  4. theorem OAI.QuarticPowerFree.determinant_dvd_of_local_expansion line 93
  5. theorem OAI.QuarticPowerFree.determinant_dvd_polynomial_eval line 127
  6. theorem OAI.QuarticPowerFree.smooth_patch_determinant_zero line 163
  7. theorem OAI.QuarticPowerFree.mv_eval_map_at line 195
  8. theorem OAI.QuarticPowerFree.intCast_isUnit_prime_power line 201
  9. theorem OAI.QuarticPowerFree.smooth_patch_determinant_dvd line 213
  10. def OAI.QuarticPowerFree.shiftVariables line 278
  11. theorem OAI.QuarticPowerFree.eval_shiftVariables line 282
  12. theorem OAI.QuarticPowerFree.pderiv_shiftVariables line 288
  13. theorem OAI.QuarticPowerFree.smooth_residue_determinant_dvd line 307
  14. theorem OAI.QuarticPowerFree.sum_min_eq_sum_card_filter line 350
  15. theorem OAI.QuarticPowerFree.monomial_order_lower_bound line 363
  16. theorem OAI.QuarticPowerFree.sum_simplex_card line 393
  17. theorem OAI.QuarticPowerFree.monomial_order_simplex_bound line 400
  18. theorem OAI.QuarticPowerFree.det_row_sum line 414
  19. theorem OAI.QuarticPowerFree.exists_relation_of_eval_dets_zero line 431
  20. theorem OAI.QuarticPowerFree.smooth_residue_determinant_simplex line 461
  21. theorem OAI.QuarticPowerFree.simultaneous_residue_determinant_dvd line 477
  22. theorem OAI.QuarticPowerFree.simultaneous_residue_determinant_zero line 500
  23. theorem OAI.QuarticPowerFree.simultaneous_residue_relation line 526