OAI/Geometry/QuadricBundles/Regularity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.baseEval_add line 9
  2. lemma OAI.QuadricCounterexample.baseEval_neg line 11
  3. lemma OAI.QuadricCounterexample.baseEval_sub line 13
  4. lemma OAI.QuadricCounterexample.baseEval_C line 15
  5. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.add line 17
  6. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.neg line 31
  7. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.sub line 36
  8. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.inv line 40
  9. lemma OAI.QuadricCounterexample.analytic_baseEval line 57
  10. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.analyticOnNhd line 69
  11. lemma OAI.QuadricCounterexample.dense_polynomial_nonzero line 79
  12. lemma OAI.QuadricCounterexample.continuous_cancel_polynomial line 98
  13. def OAI.QuadricCounterexample.UniformlyRegularOn line 119
  14. lemma OAI.QuadricCounterexample.UniformlyRegularOn.regular line 123
  15. lemma OAI.QuadricCounterexample.UniformlyRegularOn.congr line 128
  16. lemma OAI.QuadricCounterexample.UniformlyRegularOn.mono line 133
  17. lemma OAI.QuadricCounterexample.uniformlyRegular_polynomial line 138
  18. lemma OAI.QuadricCounterexample.uniformlyRegular_const line 141
  19. lemma OAI.QuadricCounterexample.UniformlyRegularOn.add line 145
  20. lemma OAI.QuadricCounterexample.UniformlyRegularOn.neg line 157
  21. lemma OAI.QuadricCounterexample.UniformlyRegularOn.sub line 161
  22. lemma OAI.QuadricCounterexample.UniformlyRegularOn.mul line 165
  23. lemma OAI.QuadricCounterexample.UniformlyRegularOn.inv line 175
  24. lemma OAI.QuadricCounterexample.UniformlyRegularOn.pow line 186
  25. lemma OAI.QuadricCounterexample.UniformlyRegularOn.eval line 192
  26. lemma OAI.QuadricCounterexample.squarefree_dvd_of_baseEval_zero line 200
  27. lemma OAI.QuadricCounterexample.exists_uniformlyRegular_division line 215