OAI/Analysis/SymmetricDomains/AnalyticImplicitScalar.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.monic_root_norm_lt_coeff_sum line 9
  2. theorem OAI.Release061.finite_fiber_of_integral_coordinates line 17
  3. theorem OAI.Release061.isCompact_preimage_of_integral_coordinates line 34
  4. theorem OAI.Release061.IsAffineAlgebraic.exists_finite_proper_polynomial_map line 80
  5. theorem OAI.Release061.finite_fiber_localization line 108
  6. theorem OAI.Release061.isProperMap_inter_preimage line 149
  7. theorem OAI.Release061.analytic_local_inverse line 164
  8. def OAI.Release061.triangularDifferentialEquiv line 185
  9. theorem OAI.Release061.triangularDifferentialEquiv_apply line 213
  10. theorem OAI.Release061.analytic_implicit_scalar line 218