OAI/Geometry/UnitDistances/Grid.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarUnitDistances.CoefficientField.FieldOf line 9
  2. def OAI.PlanarUnitDistances.CoefficientField.entry line 12
  3. theorem OAI.PlanarUnitDistances.CoefficientField.entry_val line 20
  4. theorem OAI.PlanarUnitDistances.CoefficientField.exists_left_block line 23
  5. def OAI.PlanarUnitDistances.CoefficientField.parameters line 31
  6. theorem OAI.PlanarUnitDistances.CoefficientField.parameters_zero line 34
  7. theorem OAI.PlanarUnitDistances.CoefficientField.parameters_one line 36
  8. theorem OAI.PlanarUnitDistances.CoefficientField.parameters_two line 38
  9. theorem OAI.PlanarUnitDistances.CoefficientField.parameters_three line 40
  10. theorem OAI.PlanarUnitDistances.CoefficientField.parameters_four line 42
  11. theorem OAI.PlanarUnitDistances.GridObstruction.plane line 52
  12. theorem OAI.PlanarUnitDistances.GridObstruction.curve_plane line 97
  13. theorem OAI.PlanarUnitDistances.GridObstruction.curve_curve line 166
  14. def OAI.UnitDistances.UltraField.zeroIdeal line 239
  15. theorem OAI.UnitDistances.UltraField.mem_zeroIdeal line 251
  16. instance OAI.UnitDistances.UltraField.zeroIdeal_maximal line 254
  17. abbrev OAI.UnitDistances.UltraField.FieldProduct line 266
  18. instance OAI.UnitDistances.UltraField.(instance at line 268) line 268
  19. abbrev OAI.UnitDistances.UltraField.mk line 270
  20. theorem OAI.UnitDistances.UltraField.mk_eq_mk line 272
  21. theorem OAI.UnitDistances.UltraField.mk_eq_zero line 276
  22. instance OAI.UnitDistances.UltraField.(instance at line 280) line 280
  23. theorem OAI.UnitDistances.UltraField.mk_inv line 288
  24. instance OAI.UnitDistances.UltraField.(instance at line 302) line 302
  25. abbrev OAI.PlanarUnitDistances.UltraPolynomial.bimapping line 345
  26. lemma OAI.PlanarUnitDistances.UltraPolynomial.polynomial_map_zero_iff line 348
  27. lemma OAI.PlanarUnitDistances.UltraPolynomial.bimap_zero_iff line 373
  28. lemma OAI.PlanarUnitDistances.UltraPolynomial.bimap_eq_iff line 381
  29. lemma OAI.PlanarUnitDistances.UltraPolynomial.bivariate_isUnit_iff line 386
  30. lemma OAI.PlanarUnitDistances.UltraPolynomial.bimap_unit_iff line 398
  31. lemma OAI.PlanarUnitDistances.UltraPolynomial.bimap_surjective line 408
  32. theorem OAI.PlanarUnitDistances.UltraPolynomial.irreducible_of_eventually line 411
  33. def OAI.PlanarUnitDistances.UltraPolynomial.pack line 431
  34. lemma OAI.PlanarUnitDistances.UltraPolynomial.pack_eval line 435
  35. lemma OAI.PlanarUnitDistances.UltraPolynomial.eventually_natDegree_map line 454
  36. lemma OAI.PlanarUnitDistances.UltraPolynomial.eventually_outer_degree line 481
  37. def OAI.PlanarUnitDistances.CountableCoefficients.field line 496
  38. instance OAI.PlanarUnitDistances.CountableCoefficients.(instance at line 500) line 500
  39. lemma OAI.PlanarUnitDistances.CountableCoefficients.coeff_mem_left line 507
  40. lemma OAI.PlanarUnitDistances.CountableCoefficients.coeff_mem_right line 511
  41. def OAI.PlanarUnitDistances.CountableCoefficients.descend line 515
  42. lemma OAI.PlanarUnitDistances.CountableCoefficients.descend_map line 520