OAI/Analysis/SymmetricDomains/PolynomialSignSetQuery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.signVariations_congr_coeff line 36
2. lemma OAI.Release061.SignElimination.signVariations_neg_congr_coeff line 49
3. def OAI.Release061.SignElimination.charpolyCoefficient line 59
4. lemma OAI.Release061.SignElimination.eval_charpolyCoefficient line 63
5. lemma OAI.Release061.SignElimination.rationalOn_charpoly_coefficient line 77
6. lemma OAI.Release061.SignElimination.polynomialSignSet_of_sign_invariant line 84
7. def OAI.Release061.SignElimination.coefficientHermiteMatrix line 103
8. lemma OAI.Release061.SignElimination.coefficientHermiteMatrix_eq line 108
9. lemma OAI.Release061.SignElimination.rationalOn_coefficientHermite line 115
10. lemma OAI.Release061.SignElimination.tarskiQuery_coefficient_charpoly line 128
11. theorem OAI.Release061.SignElimination.polynomialSignSet_query_predicate line 137