OAI/Analysis/SymmetricDomains/FiniteProperMapOpen.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.finite_algebra_generic_sheets_constant_degree line 16
  2. def OAI.Release061.quotientCoordinate line 117
  3. def OAI.Release061.affineCharacter line 121
  4. theorem OAI.Release061.affineCharacter_mk line 125
  5. theorem OAI.Release061.affineCharacter_coordinate line 129
  6. theorem OAI.Release061.character_comp_mk line 135
  7. def OAI.Release061.pointOfCharacter line 142
  8. def OAI.Release061.affineCharacterEquiv line 150
  9. theorem OAI.Release061.continuous_affineCharacter line 163
  10. theorem OAI.Release061.adjoin_quotientCoordinate line 169
  11. theorem OAI.Release061.affineCharacter_normalization line 177
  12. theorem OAI.Release061.polynomial_root_near_of_small_eval line 189
  13. theorem OAI.Release061.polynomial_eventually_exists_near_root line 208
  14. theorem OAI.Release061.finite_proper_map_open_at_of_root_realization line 229