OAI/NumberTheory/Jacobsthal/Estimates/FactorDividesAbscissa.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseIncidence.bit line 16
  2. def OAI.Erdos970.ErdosInverseIncidence.degree line 17
  3. def OAI.Erdos970.ErdosInverseIncidence.multiplicity line 19
  4. theorem OAI.Erdos970.ErdosInverseIncidence.bit_nonneg line 22
  5. theorem OAI.Erdos970.ErdosInverseIncidence.sum_bit line 26
  6. theorem OAI.Erdos970.ErdosInverseIncidence.sum_bit_product line 30
  7. theorem OAI.Erdos970.ErdosInverseIncidence.multiplicity_sum line 37
  8. theorem OAI.Erdos970.ErdosInverseIncidence.multiplicity_square_sum line 43
  9. theorem OAI.Erdos970.ErdosInverseIncidence.multiplicity_square_upper line 57
  10. theorem OAI.Erdos970.ErdosInverseIncidence.dense_incidence_card_bound line 83
  11. def OAI.Erdos970.ErdosInverseAlignment.aligns line 131
  12. theorem OAI.Erdos970.ErdosInverseAlignment.aligns_iff_modEq line 134
  13. theorem OAI.Erdos970.ErdosInverseAlignment.aligned_prime_not_dvd_den line 139
  14. def OAI.Erdos970.ErdosInverseAlignment.determinant line 151
  15. theorem OAI.Erdos970.ErdosInverseAlignment.determinant_ne_zero line 153
  16. theorem OAI.Erdos970.ErdosInverseAlignment.common_alignment_dvd line 159
  17. def OAI.Erdos970.ErdosInverseAlignment.commonAligners line 168
  18. theorem OAI.Erdos970.ErdosInverseAlignment.commonAligners_le_divisors line 171
  19. theorem OAI.Erdos970.ErdosInverseAlignment.determinant_height line 180
  20. theorem OAI.Erdos970.ErdosInverseAlignment.commonAligners_subpower line 191
  21. def OAI.Erdos970.ErdosInverseAlignment.heightCandidates line 216
  22. theorem OAI.Erdos970.ErdosInverseAlignment.mem_heightCandidates line 221
  23. def OAI.Erdos970.ErdosInverseAlignment.rationalList line 239
  24. theorem OAI.Erdos970.ErdosInverseAlignment.mem_rationalList line 243
  25. theorem OAI.Erdos970.ErdosInverseAlignment.rational_list_card_subpower line 249
  26. theorem OAI.Erdos970.ErdosRichLine.linear_y_coefficient_ne_zero line 277
  27. theorem OAI.Erdos970.ErdosRichLine.linear_integer_cross_product line 293
  28. structure OAI.Erdos970.ErdosRichLine.PrimitiveIntegerLine line 317
  29. def OAI.Erdos970.ErdosRichLine.PrimitiveIntegerLine.Contains line 324
  30. theorem OAI.Erdos970.ErdosRichLine.primitive_line_from_cross_products line 327
  31. theorem OAI.Erdos970.ErdosRichLine.primitive_line_of_polynomial line 346
  32. structure OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction line 364
  33. theorem OAI.Erdos970.ErdosPrimitiveIntercept.exists_intercept_reduction line 371
  34. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.rational_value line 393
  35. theorem OAI.Erdos970.ErdosRichLine.exists_rich_primitive_line line 410
  36. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.factor_dvd_denominator line 440
  37. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.factor_dvd_abscissa line 443