OAI/Geometry/QuadricBundles/LineFactors.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuadricCounterexample.StandardChart line 9
  2. def OAI.QuadricCounterexample.overlapPolynomial line 11
  3. def OAI.QuadricCounterexample.coordinateOverlap line 13
  4. def OAI.QuadricCounterexample.scalarCoordinateChange line 15
  5. def OAI.QuadricCounterexample.coordinateChange line 16
  6. def OAI.QuadricCounterexample.scalarFactor line 18
  7. def OAI.QuadricCounterexample.firstFactor line 20
  8. def OAI.QuadricCounterexample.secondFactor line 21
  9. lemma OAI.QuadricCounterexample.coordinateOverlap_iff line 23
  10. lemma OAI.QuadricCounterexample.scalarCoordinateChange_coord line 28
  11. lemma OAI.QuadricCounterexample.coordinateChange_coord line 40
  12. lemma OAI.QuadricCounterexample.scalarCoordinateChange_self line 44
  13. lemma OAI.QuadricCounterexample.coordinateChange_self line 46
  14. lemma OAI.QuadricCounterexample.scalarCoordinateChange_inv line 48
  15. lemma OAI.QuadricCounterexample.coordinateChange_inv line 51
  16. lemma OAI.QuadricCounterexample.affineP1_mem_range line 55
  17. lemma OAI.QuadricCounterexample.affineQuadric_mem_range line 66
  18. lemma OAI.QuadricCounterexample.affine_coordinateChange line 71
  19. lemma OAI.QuadricCounterexample.coordinateOverlap_change line 77
  20. lemma OAI.QuadricCounterexample.coordinateChange_comp line 82
  21. lemma OAI.QuadricCounterexample.coordinateOverlap_third line 87
  22. lemma OAI.QuadricCounterexample.coordinateOverlap_open line 93
  23. lemma OAI.QuadricCounterexample.uniformlyRegular_fst line 96
  24. lemma OAI.QuadricCounterexample.uniformlyRegular_snd line 98
  25. lemma OAI.QuadricCounterexample.UniformlyRegularOn.comp line 101
  26. lemma OAI.QuadricCounterexample.firstFactor_regular line 118
  27. lemma OAI.QuadricCounterexample.secondFactor_regular line 124
  28. lemma OAI.QuadricCounterexample.firstFactor_ne_zero line 131
  29. lemma OAI.QuadricCounterexample.secondFactor_ne_zero line 138
  30. lemma OAI.QuadricCounterexample.coordinateChange_fst_regular line 146
  31. lemma OAI.QuadricCounterexample.coordinateChange_snd_regular line 155
  32. lemma OAI.QuadricCounterexample.firstFactor_transition line 165
  33. lemma OAI.QuadricCounterexample.secondFactor_transition line 168
  34. lemma OAI.QuadricCounterexample.firstFactor_mul line 172
  35. lemma OAI.QuadricCounterexample.secondFactor_mul line 180