OAI/NumberTheory/PowerFree/ComplexValues.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.tripleFinsuppEquiv line 9
  2. def OAI.QuarticPowerFree.tripleWeights line 16
  3. theorem OAI.QuarticPowerFree.weight_eq_tripleWeight line 18
  4. theorem OAI.QuarticPowerFree.tripleWeights_ne_zero line 23
  5. theorem OAI.QuarticPowerFree.weightedExponents_card line 28
  6. theorem OAI.QuarticPowerFree.weighted_hypersurface_normal_card line 37
  7. theorem OAI.QuarticPowerFree.surface_hilbert_error line 52
  8. theorem OAI.QuarticPowerFree.ComplexValues.denominator_value_dvd_resultant line 81
  9. theorem OAI.QuarticPowerFree.ComplexValues.card_fibre_eval_le line 91
  10. def OAI.QuarticPowerFree.ComplexValues.signedDivisors line 105
  11. theorem OAI.QuarticPowerFree.ComplexValues.mem_signedDivisors line 109
  12. theorem OAI.QuarticPowerFree.ComplexValues.card_signedDivisors_le line 119
  13. theorem OAI.QuarticPowerFree.ComplexValues.rational_values_card_le_divisors line 126
  14. theorem OAI.QuarticPowerFree.ComplexValues.rational_function_interpolation_cross line 151
  15. theorem OAI.QuarticPowerFree.ComplexValues.rational_function_interpolation_unique line 166
  16. def OAI.QuarticPowerFree.ComplexValues.interpolationRow line 191
  17. theorem OAI.QuarticPowerFree.ComplexValues.interpolationRow_some_dot line 197
  18. theorem OAI.QuarticPowerFree.ComplexValues.interpolationRow_none_dot line 212
  19. def OAI.QuarticPowerFree.ComplexValues.interpolationMatrix line 217
  20. theorem OAI.QuarticPowerFree.ComplexValues.interpolationMatrix_det_ne_zero line 222
  21. theorem OAI.QuarticPowerFree.ComplexValues.ofFn_map_hom line 278
  22. theorem OAI.QuarticPowerFree.ComplexValues.interpolationMatrix_map line 287
  23. def OAI.QuarticPowerFree.ComplexValues.interpolationCramer line 304
  24. theorem OAI.QuarticPowerFree.ComplexValues.rational_interpolation_integral_pair line 310
  25. theorem OAI.QuarticPowerFree.ComplexValues.det_abs_le_row_product line 382
  26. theorem OAI.QuarticPowerFree.ComplexValues.det_abs_le_uniform line 404
  27. theorem OAI.QuarticPowerFree.ComplexValues.interpolationRow_abs_le line 411
  28. theorem OAI.QuarticPowerFree.ComplexValues.interpolationCramer_abs_le line 440
  29. def OAI.QuarticPowerFree.ComplexValues.interpolationHeight line 463
  30. theorem OAI.QuarticPowerFree.ComplexValues.interpolationHeight_one_le line 466
  31. theorem OAI.QuarticPowerFree.ComplexValues.interpolationCramer_abs_le_degree_bound line 471
  32. theorem OAI.QuarticPowerFree.ComplexValues.resultant_abs_le_coeff_bound line 484
  33. theorem OAI.QuarticPowerFree.ComplexValues.resultant_ne_zero_of_scalar_maps line 504
  34. theorem OAI.QuarticPowerFree.ComplexValues.rational_interpolation_height line 522
  35. theorem OAI.QuarticPowerFree.ComplexValues.eval_eq_mul_of_scalar_maps line 560
  36. theorem OAI.QuarticPowerFree.ComplexValues.rational_values_height_representative line 573
  37. def OAI.QuarticPowerFree.ComplexValues.rationalResultantConstant line 600
  38. def OAI.QuarticPowerFree.ComplexValues.rationalResultantExponent line 603
  39. theorem OAI.QuarticPowerFree.ComplexValues.rationalResultantConstant_pos line 605
  40. theorem OAI.QuarticPowerFree.ComplexValues.rationalResultantExponent_pos line 609
  41. theorem OAI.QuarticPowerFree.ComplexValues.resultant_abs_le_interpolation_height line 614
  42. theorem OAI.QuarticPowerFree.ComplexValues.succ_le_geometric line 638
  43. theorem OAI.QuarticPowerFree.ComplexValues.divisors_card_le_rpow line 646
  44. theorem OAI.QuarticPowerFree.ComplexValues.rational_values_card_le_rpow line 702
  45. theorem OAI.QuarticPowerFree.ComplexValues.rational_integer_values_uniform line 773