OAI/Analysis/SymmetricDomains/GenericTangentComplexNormal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.independent_functionals_surjective line 35
2. theorem OAI.Release061.exists_scalar_continuousLinearEquiv_prod_ker line 65
3. lemma OAI.Release061.submodule_basis_independent line 98
4. lemma OAI.Release061.real_conormal_basis_complex_independent line 103
5. lemma OAI.Release061.real_conormal_basis_vanishing_iff line 120
6. theorem OAI.Release061.generic_tangent_complex_normal_form line 137