OAI/Analysis/SymmetricDomains/TarskiQueryCharpoly.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.quadratic_matrix_apply line 40
2. lemma OAI.Release061.SignElimination.quadratic_matrix_comp line 44
3. lemma OAI.Release061.SignElimination.diagonal_quadratic line 52
4. lemma OAI.Release061.SignElimination.quadratic_signature_eigenvalues line 63
5. lemma OAI.Release061.SignElimination.signature_matrix_charpoly line 81
6. def OAI.Release061.SignElimination.hermiteMatrix line 98
7. lemma OAI.Release061.SignElimination.hermiteMatrix_isHermitian line 102
8. lemma OAI.Release061.SignElimination.root_matrix_identity line 108
9. lemma OAI.Release061.SignElimination.complexify_eval_degreeLT line 124
10. lemma OAI.Release061.SignElimination.hermiteMatrix_quadratic line 130
11. lemma OAI.Release061.SignElimination.hermiteMatrix_signature line 155
12. lemma OAI.Release061.SignElimination.hermiteMatrix_coefficients line 162
13. theorem OAI.Release061.SignElimination.tarskiQuery_charpoly line 188