OAI/Geometry/UnitDistances/Valuations.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarUnitDistances.Radicals.exp_neg_one_ne_square line 11
  2. theorem OAI.PlanarUnitDistances.Radicals.squareIndependent_of_private_valuations line 17
  3. def OAI.PlanarUnitDistances.Radicals.pointPrime line 47
  4. def OAI.PlanarUnitDistances.Radicals.pointValuation line 56
  5. theorem OAI.PlanarUnitDistances.Radicals.pointValuation_polynomial_of_eval_ne_zero line 59
  6. theorem OAI.PlanarUnitDistances.Radicals.pointValuation_X_sub_C line 65
  7. theorem OAI.PlanarUnitDistances.Radicals.pointValuation_of_simple_root line 71
  8. theorem OAI.PlanarUnitDistances.Radicals.squareIndependent_of_private_simple_roots line 81
  9. lemma OAI.PlanarUnitDistances.Radicals.ratFunc_X_sub_C_ne_zero line 101
  10. def OAI.PlanarUnitDistances.Radicals.planePrivateRoot line 105
  11. lemma OAI.PlanarUnitDistances.Radicals.planePrivateRoot_ne_constant line 109
  12. lemma OAI.PlanarUnitDistances.Radicals.planePrivateRoot_injective line 120
  13. def OAI.PlanarUnitDistances.Radicals.planeDistancePoly line 145
  14. def OAI.PlanarUnitDistances.Radicals.planeRadicandPoly line 148
  15. lemma OAI.PlanarUnitDistances.Radicals.planePrivateRoot_distance line 152
  16. lemma OAI.PlanarUnitDistances.Radicals.planePrivateRoot_simple line 158
  17. lemma OAI.PlanarUnitDistances.Radicals.planePrivateRoot_other line 170
  18. theorem OAI.PlanarUnitDistances.Radicals.plane_radicands_squareIndependent line 185
  19. lemma OAI.PlanarUnitDistances.Radicals.independent_difference_ne line 205
  20. def OAI.PlanarUnitDistances.Radicals.lineDistancePoly line 218
  21. def OAI.PlanarUnitDistances.Radicals.lineRadicandPoly line 220
  22. lemma OAI.PlanarUnitDistances.Radicals.line_root_simple line 225
  23. lemma OAI.PlanarUnitDistances.Radicals.line_root_other line 240
  24. theorem OAI.PlanarUnitDistances.Radicals.line_radicands_squareIndependent line 272
  25. theorem OAI.PlanarUnitDistances.Radicals.line_radicands_squareIndependent_over_constants line 288
  26. lemma OAI.PlanarUnitDistances.Radicals.independent_affine_ne line 314
  27. lemma OAI.PlanarUnitDistances.Radicals.circle_aux_root line 327
  28. def OAI.PlanarUnitDistances.Radicals.circleNumerator line 352
  29. def OAI.PlanarUnitDistances.Radicals.circleDenominator line 353
  30. def OAI.PlanarUnitDistances.Radicals.circleDifference line 354
  31. def OAI.PlanarUnitDistances.Radicals.circleRadicandNumerator line 356
  32. def OAI.PlanarUnitDistances.Radicals.circleDistance line 359
  33. def OAI.PlanarUnitDistances.Radicals.circleRadicand line 362
  34. lemma OAI.PlanarUnitDistances.Radicals.circleRadicand_eq_fraction line 366
  35. lemma OAI.PlanarUnitDistances.Radicals.circle_root_simple line 376
  36. lemma OAI.PlanarUnitDistances.Radicals.circle_root_other line 415
  37. theorem OAI.PlanarUnitDistances.Radicals.circle_radicands_squareIndependent line 460
  38. theorem OAI.PlanarUnitDistances.Radicals.circle_radicands_squareIndependent_over_constants line 495
  39. def OAI.PlanarUnitDistances.GenericCurve.ratEval line 525
  40. lemma OAI.PlanarUnitDistances.GenericCurve.ratEval_polynomial line 528
  41. lemma OAI.PlanarUnitDistances.GenericCurve.ratEval_comp line 534
  42. lemma OAI.PlanarUnitDistances.GenericCurve.ratEval_X line 538
  43. lemma OAI.PlanarUnitDistances.GenericCurve.ratEval_C line 542
  44. lemma OAI.PlanarUnitDistances.GenericCurve.irreducible_fraction_curve line 546
  45. theorem OAI.PlanarUnitDistances.GenericCurve.exists_curve_embedding line 551
  46. lemma OAI.PlanarUnitDistances.GenericCurve.fiber_separable line 567
  47. lemma OAI.PlanarUnitDistances.GenericCurve.fiber_degree line 574
  48. lemma OAI.PlanarUnitDistances.GenericCurve.fiber_leadingCoeff_ne_zero line 578
  49. lemma OAI.PlanarUnitDistances.GenericCurve.separable_exists_root_ne line 584
  50. theorem OAI.PlanarUnitDistances.GenericCurve.exists_distinct_smooth_sheet line 601
  51. theorem OAI.PlanarUnitDistances.GenericPlane.exists_plane_embedding line 630
  52. theorem OAI.PlanarUnitDistances.Radicals.plane_differential_obstruction line 674
  53. theorem OAI.PlanarUnitDistances.Radicals.line_differential_obstruction line 710
  54. lemma OAI.PlanarUnitDistances.Radicals.circleDistance_is_locus_distance line 756
  55. theorem OAI.PlanarUnitDistances.Radicals.circle_differential_obstruction line 779