OAI/Analysis/SymmetricDomains/IntegralPrimitive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.glue_dense_differentiable_extensions line 12
  2. theorem OAI.Release061.bounded_polynomial_removable line 44
  3. theorem OAI.Release061.resultant_derivative_ne_zero_of_generic_separable line 61
  4. theorem OAI.Release061.eval₂_derivative_ne_zero_of_resultant line 75
  5. theorem OAI.Release061.separable_map_of_resultant_ne_zero line 93
  6. theorem OAI.Release061.integral_minpoly_resultant_ne_zero line 113
  7. theorem OAI.Release061.polynomial_analytic_sheets line 123
  8. theorem OAI.Release061.exists_integral_primitive line 202