OAI/Geometry/UnitDistances/GenericCurves.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.GenericNoncoincidence.poleTest line 9
  2. lemma OAI.PlanarUnitDistances.GenericNoncoincidence.poleTest_eval_center line 12
  3. lemma OAI.PlanarUnitDistances.GenericNoncoincidence.poleTest_nonzero line 26
  4. theorem OAI.PlanarUnitDistances.GenericNoncoincidence.distance_ne_nonzero line 34
  5. lemma OAI.PlanarUnitDistances.GenericNoncoincidence.primitive_fiber_ne_zero line 55
  6. lemma OAI.PlanarUnitDistances.GenericNoncoincidence.aevalAeval_eq_eval₂ line 66
  7. theorem OAI.PlanarUnitDistances.GenericNoncoincidence.generic_ordinate_ne_constant line 76
  8. abbrev OAI.PlanarUnitDistances.BivariateMaps.bimap line 100
  9. lemma OAI.PlanarUnitDistances.BivariateMaps.bimap_injective line 103
  10. lemma OAI.PlanarUnitDistances.BivariateMaps.isUnit_bimap_iff line 106
  11. lemma OAI.PlanarUnitDistances.BivariateMaps.irreducible_of_bimap line 126
  12. lemma OAI.PlanarUnitDistances.BivariateMaps.bimap_comp line 135
  13. lemma OAI.PlanarUnitDistances.BivariateMaps.bimap_natDegree line 139
  14. lemma OAI.PlanarUnitDistances.BivariateMaps.bimap_swap line 143
  15. lemma OAI.PlanarUnitDistances.BivariateMaps.eval_bimap line 153
  16. lemma OAI.PlanarUnitDistances.GenericSheets.fiber_algebraic line 167
  17. lemma OAI.PlanarUnitDistances.GenericSheets.other_transcendental line 187
  18. theorem OAI.PlanarUnitDistances.GenericSheets.exists_private_sheet_curve line 196
  19. lemma OAI.PlanarUnitDistances.GenericSheets.bivariate_eval_ne_zero line 255
  20. lemma OAI.PlanarUnitDistances.GenericSheets.other_block_independent line 268
  21. lemma OAI.PlanarUnitDistances.GenericSheets.independent_distance_ne line 287
  22. theorem OAI.PlanarUnitDistances.GenericSheets.exists_private_sheet_plane line 299
  23. theorem OAI.PlanarUnitDistances.CurveValuations.powerSeries_simple_root line 344
  24. def OAI.PlanarUnitDistances.CurveValuations.shiftPowerSeries line 376
  25. lemma OAI.PlanarUnitDistances.CurveValuations.shiftPowerSeries_injective line 379
  26. lemma OAI.PlanarUnitDistances.CurveValuations.shiftPowerSeries_C line 382
  27. lemma OAI.PlanarUnitDistances.CurveValuations.shiftPowerSeries_X line 386
  28. lemma OAI.PlanarUnitDistances.CurveValuations.constantCoeff_comp_shiftPowerSeries line 390
  29. lemma OAI.PlanarUnitDistances.CurveValuations.constantCoeff_shiftPowerSeries line 394
  30. def OAI.PlanarUnitDistances.CurveValuations.shiftLaurent line 398
  31. lemma OAI.PlanarUnitDistances.CurveValuations.shiftLaurent_injective line 401
  32. lemma OAI.PlanarUnitDistances.CurveValuations.shiftLaurent_regular line 404
  33. def OAI.PlanarUnitDistances.CurveValuations.shiftRatFunc line 414
  34. lemma OAI.PlanarUnitDistances.CurveValuations.shiftRatFunc_polynomial line 417
  35. lemma OAI.PlanarUnitDistances.CurveValuations.shiftRatFunc_comp_algebraMap line 421
  36. theorem OAI.PlanarUnitDistances.CurveValuations.exists_smooth_branch line 425
  37. abbrev OAI.PlanarUnitDistances.CurveValuations.CurveField line 439
  38. theorem OAI.PlanarUnitDistances.CurveValuations.exists_curve_branch_map line 441
  39. lemma OAI.PlanarUnitDistances.CurveValuations.laurent_valuation_powerSeries_unit line 460
  40. lemma OAI.PlanarUnitDistances.CurveValuations.laurent_valuation_powerSeries_X line 468
  41. def OAI.PlanarUnitDistances.CurveValuations.curveZ line 473
  42. def OAI.PlanarUnitDistances.CurveValuations.curveC line 476
  43. def OAI.PlanarUnitDistances.CurveValuations.curveL line 479
  44. def OAI.PlanarUnitDistances.CurveValuations.curveD line 482
  45. lemma OAI.PlanarUnitDistances.CurveValuations.curve_branch_map_of line 485
  46. lemma OAI.PlanarUnitDistances.CurveValuations.curve_branch_map_L line 492
  47. theorem OAI.PlanarUnitDistances.CurveValuations.exists_curve_private_valuation line 506
  48. theorem OAI.PlanarUnitDistances.Radicals.curve_differential_obstruction line 561
  49. lemma OAI.PlanarUnitDistances.GenericSheets.mapped_leading_eval line 610
  50. lemma OAI.PlanarUnitDistances.GenericSheets.mapped_eval line 618
  51. lemma OAI.PlanarUnitDistances.GenericSheets.mapped_derivative_eval line 625
  52. theorem OAI.PlanarUnitDistances.Radicals.curve_curve_differential_obstruction line 639
  53. theorem OAI.PlanarUnitDistances.Radicals.curve_plane_differential_obstruction line 666