OAI/NumberTheory/Jacobsthal/Estimates/RichLinearFactor.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosComplexCurveFactors.complexPolynomialNormalization line 14
  2. theorem OAI.Erdos970.ErdosComplexCurveFactors.associated_constant line 19
  3. theorem OAI.Erdos970.ErdosComplexCurveFactors.associated_totalDegree line 25
  4. theorem OAI.Erdos970.ErdosComplexCurveFactors.associated_squarePoints line 29
  5. theorem OAI.Erdos970.ErdosComplexCurveFactors.irreducible_totalDegree_pos line 34
  6. theorem OAI.Erdos970.ErdosComplexCurveFactors.totalDegree_multiset_prod line 46
  7. theorem OAI.Erdos970.ErdosComplexCurveFactors.multiset_card_le_degree_sum line 57
  8. theorem OAI.Erdos970.ErdosComplexCurveFactors.normalizedFactors_card_le_degree line 67
  9. def OAI.Erdos970.ErdosComplexCurveFactors.nonlinearFactors line 75
  10. theorem OAI.Erdos970.ErdosComplexCurveFactors.mem_nonlinearFactors line 79
  11. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonlinearFactors_card_le_degree line 84
  12. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonlinearFactor_degree_le line 90
  13. def OAI.Erdos970.ErdosComplexCurveFactors.OnNonlinearComponent line 107
  14. def OAI.Erdos970.ErdosComplexCurveFactors.nonlinearSquarePoints line 111
  15. theorem OAI.Erdos970.ErdosComplexCurveFactors.mem_nonlinearSquarePoints line 114
  16. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonlinearSquare_eq_union line 119
  17. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonlinear_square_degree_four_bound line 151
  18. theorem OAI.Erdos970.ErdosComplexCurveFactors.nonlinear_square_bound_of_degree_le line 179
  19. def OAI.Erdos970.ErdosComplexCurveFactors.realNonlinearSquarePoints line 195
  20. theorem OAI.Erdos970.ErdosComplexCurveFactors.mem_realNonlinearSquarePoints line 198
  21. theorem OAI.Erdos970.ErdosComplexCurveFactors.complexify_ne_zero line 204
  22. theorem OAI.Erdos970.ErdosComplexCurveFactors.degree_uniform_nonlinear_lattice_bound line 210
  23. theorem OAI.Erdos970.ErdosComplexCurveFactors.exists_absolute_nonlinear_bound line 216
  24. def OAI.Erdos970.ErdosRichLine.linearFactors line 235
  25. theorem OAI.Erdos970.ErdosRichLine.mem_linearFactors line 239
  26. theorem OAI.Erdos970.ErdosRichLine.linearFactors_card_le_degree line 244
  27. theorem OAI.Erdos970.ErdosRichLine.zero_mem_normalized_factor line 250
  28. theorem OAI.Erdos970.ErdosRichLine.square_zero_cover line 264
  29. theorem OAI.Erdos970.ErdosRichLine.selected_point_cover line 290
  30. theorem OAI.Erdos970.ErdosRichLine.selected_count_bound line 301
  31. theorem OAI.Erdos970.ErdosRichLine.exists_rich_linear_factor line 321