OAI/Analysis/SymmetricDomains/PolynomialSignSetFinite.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.PolynomialSignSet.univ line 38
2. lemma OAI.Release061.PolynomialSignSet.empty line 39
3. lemma OAI.Release061.PolynomialSignSet.inter line 40
4. lemma OAI.Release061.PolynomialSignSet.const line 43
5. lemma OAI.Release061.PolynomialSignSet.exists_finset line 48
6. lemma OAI.Release061.PolynomialSignSet.exists_finite line 60
7. lemma OAI.Release061.PolynomialSignSet.forall_finite line 66
8. lemma OAI.Release061.PolynomialSignSet.sign line 73
9. def OAI.Release061.SignElimination.RationalOn line 86
10. lemma OAI.Release061.SignElimination.RationalOn.congr line 93
11. lemma OAI.Release061.SignElimination.RationalOn.mono line 97
12. lemma OAI.Release061.SignElimination.RationalOn.polynomial line 101
13. lemma OAI.Release061.SignElimination.RationalOn.const line 104
14. lemma OAI.Release061.SignElimination.RationalOn.add line 107
15. lemma OAI.Release061.SignElimination.RationalOn.neg line 118
16. lemma OAI.Release061.SignElimination.RationalOn.sub line 122
17. lemma OAI.Release061.SignElimination.RationalOn.mul line 125
18. lemma OAI.Release061.SignElimination.RationalOn.pow line 132
19. lemma OAI.Release061.SignElimination.RationalOn.inv line 137
20. lemma OAI.Release061.SignElimination.RationalOn.div line 147
21. lemma OAI.Release061.SignElimination.RationalOn.sum line 151
22. lemma OAI.Release061.SignElimination.RationalOn.eval line 159
23. lemma OAI.Release061.SignElimination.RationalOn.sign_inv_real line 167
24. lemma OAI.Release061.SignElimination.RationalOn.sign_set line 173
25. lemma OAI.Release061.SignElimination.polynomialSignSet_finite_signs line 188