OAI/Analysis/SymmetricDomains/SignVariationsPositiveRoots.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.coeff_comp_neg line 35
2. lemma OAI.Release061.SignElimination.natDegree_comp_neg line 39
3. lemma OAI.Release061.SignElimination.eraseLead_comp_neg line 42
4. lemma OAI.Release061.SignElimination.sign_pair_indicator line 48
5. lemma OAI.Release061.SignElimination.signVariations_pair_le line 53
6. lemma OAI.Release061.SignElimination.coeffList_mul_X line 79
7. lemma OAI.Release061.SignElimination.signVariations_mul_X line 88
8. lemma OAI.Release061.SignElimination.positive_negative_roots_card line 93
9. theorem OAI.Release061.SignElimination.signVariations_eq_positive_roots line 107