OAI/Analysis/SymmetricDomains/HermiteSignature.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.SignElimination.complexEvaluation line 37
2. lemma OAI.Release061.SignElimination.complexEvaluation_apply line 40
3. def OAI.Release061.SignElimination.rootSquare line 45
4. lemma OAI.Release061.SignElimination.rootSquare_apply line 50
5. def OAI.Release061.SignElimination.hermiteForm line 54
6. lemma OAI.Release061.SignElimination.hermiteForm_apply line 57
7. lemma OAI.Release061.SignElimination.rootEvaluation_real line 62
8. lemma OAI.Release061.SignElimination.rootEvaluation_upper line 66
9. lemma OAI.Release061.SignElimination.hermiteForm_root_values line 72
10. theorem OAI.Release061.SignElimination.hermite_signature line 104