OAI/Analysis/SymmetricDomains/RealCriticalMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.realCriticalMatrix line 35
2. def OAI.Release061.realCriticalConstant line 42
3. lemma OAI.Release061.realCriticalMatrix_apply line 45
4. lemma OAI.Release061.realCriticalMatrix_surjective line 51
5. lemma OAI.Release061.realCriticalMatrix_contDiffAt line 70
6. lemma OAI.Release061.realCriticalConstant_contDiffAt line 81
7. theorem OAI.Release061.realCriticalMatrix_eq_iff line 87