OAI/Geometry/UnitDistances/Radicals.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.Radicals.SquareIndependent line 9
  2. theorem OAI.PlanarUnitDistances.Radicals.square_in_quadratic_iff line 16
  3. def OAI.PlanarUnitDistances.Radicals.quadraticFlip line 36
  4. theorem OAI.PlanarUnitDistances.Radicals.quadraticFlip_cast line 45
  5. theorem OAI.PlanarUnitDistances.Radicals.quadraticFlip_omega line 50
  6. def OAI.PlanarUnitDistances.Radicals.quadraticLift line 55
  7. theorem OAI.PlanarUnitDistances.Radicals.quadraticLift_cast line 64
  8. theorem OAI.PlanarUnitDistances.Radicals.quadraticLift_omega line 68
  9. def OAI.PlanarUnitDistances.Radicals.quadraticEval line 73
  10. theorem OAI.PlanarUnitDistances.Radicals.quadraticEval_cast line 86
  11. theorem OAI.PlanarUnitDistances.Radicals.quadraticEval_omega line 92
  12. structure OAI.PlanarUnitDistances.Radicals.RadicalModel line 99
  13. def OAI.PlanarUnitDistances.Radicals.emptyModel line 121
  14. theorem OAI.PlanarUnitDistances.Radicals.tail_independent line 141
  15. theorem OAI.PlanarUnitDistances.Radicals.head_not_square line 147
  16. theorem OAI.PlanarUnitDistances.Radicals.head_ne_zero line 157
  17. theorem OAI.PlanarUnitDistances.Radicals.extend_square_descends line 164
  18. def OAI.PlanarUnitDistances.Radicals.extendModel line 194
  19. theorem OAI.PlanarUnitDistances.Radicals.exists_radicalModel line 243
  20. theorem OAI.PlanarUnitDistances.Radicals.SquareIndependent.get_ne_zero line 259
  21. theorem OAI.PlanarUnitDistances.Radicals.RadicalModel.root_ne_zero line 268
  22. theorem OAI.PlanarUnitDistances.Radicals.RadicalModel.linear_relation line 277
  23. theorem OAI.PlanarUnitDistances.Radicals.actual_roots_linear_relation line 302
  24. theorem OAI.PlanarUnitDistances.Radicals.actual_sign_changes line 312
  25. theorem OAI.PlanarUnitDistances.Radicals.solution_lift_fixed line 341
  26. theorem OAI.PlanarUnitDistances.Radicals.unused_sign_equation line 367
  27. theorem OAI.PlanarUnitDistances.Radicals.planar_radical_forces_scalar line 382
  28. theorem OAI.PlanarUnitDistances.Radicals.line_radical_forces_scalar line 449
  29. theorem OAI.PlanarUnitDistances.Radicals.radical_system_impossible line 508
  30. theorem OAI.UnitDistances.DifferentialSystem.logDerivative_factorization line 547
  31. theorem OAI.UnitDistances.DifferentialSystem.edge_radicand line 555
  32. theorem OAI.UnitDistances.DifferentialSystem.differentiated_distance line 561
  33. theorem OAI.UnitDistances.DifferentialSystem.differentiated_edge line 574
  34. theorem OAI.UnitDistances.DifferentialSystem.differentiated_zw line 598
  35. theorem OAI.PlanarUnitDistances.Radicals.differential_distance_obstruction line 613