OAI/Analysis/SymmetricDomains/Model.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.linearConjugateChart line 37
2. lemma OAI.Release061.linearConjugateChart_source line 42
3. lemma OAI.Release061.linearConjugateChart_target line 47
4. lemma OAI.Release061.linearConjugateChart_apply line 52
5. lemma OAI.Release061.linearConjugateChart_symm_apply line 56
6. lemma OAI.Release061.linearConjugateChart_analytic line 60
7. lemma OAI.Release061.linearConjugateChart_inverse_analytic line 67
8. lemma OAI.Release061.linearConjugateChart_image line 74
9. theorem OAI.Release061.model_bounded_biholomorph line 82