OAI/Analysis/SymmetricDomains/AmbientInverse.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.zeroLocus_maximum_local line 16
  2. theorem OAI.Release061.scalar_maximum_local_of_holomorphy line 63
  3. theorem OAI.Release061.scalar_maximum_of_holomorphy line 110
  4. theorem OAI.Release061.scalar_singular_montel line 121
  5. theorem OAI.Release061.integral_minpoly_constant_ne_zero line 133
  6. theorem OAI.Release061.dense_character_nonzero line 145
  7. theorem OAI.Release061.prime_zeroLocus_dense_polynomial_nonzero line 164
  8. theorem OAI.Release061.finite_sheet_isolating_neighborhood line 185
  9. theorem OAI.Release061.holomorphicOnSubset_of_analyticOnNhd line 218
  10. def OAI.Release061.biholomorphOfAmbientInverse line 225