OAI/Analysis/SymmetricDomains/PolynomialRemovableLocal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.bounded_removable_finite line 12
  2. theorem OAI.Release061.bounded_removable_finite_fibers line 66
  3. def OAI.Release061.linePolynomial line 117
  4. theorem OAI.Release061.eval_linePolynomial line 121
  5. theorem OAI.Release061.exists_eval_ne_zero line 136
  6. theorem OAI.Release061.polynomial_eventually_ne_zero line 141
  7. theorem OAI.Release061.exists_polynomial_root_free_sphere line 150
  8. theorem OAI.Release061.dense_polynomial_nonzero line 172
  9. theorem OAI.Release061.finite_polynomial_line_roots line 188
  10. theorem OAI.Release061.bounded_polynomial_removable_local line 202