Related questions
🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ537 | |
| 2 | Ṁ126 | |
| 3 | Ṁ64 | |
| 4 | Ṁ63 | |
| 5 | Ṁ48 |
Tried to look for PRs that mention theorems from the list of the 26 theorems that are not added yet:
Old PRs that should be adopted:
https://github.com/leanprover-community/mathlib/pull/10632 - Ceva's theorem, requires changes
https://github.com/leanprover-community/mathlib/pull/2819 - Minkowsky's theorem, I don't know what's up here, the PR seems kinda old and abandoned
Also:
this PR says it should be useful for Descartes' rule of signs: https://github.com/leanprover-community/mathlib/pull/14949
in https://github.com/leanprover-community/mathlib/pull/16615, @mlavrent mentions working on Brouwer fixed point theorem, but I don't know where his PR is
@JoachimBreitner Apparently Brouwer's fixed point theorem is done but not PRed. I think Hermite-Lindemann was being worked on too recently. I myself was working on Descartes' Rule of Signs through #14916, you are welcome to adopt that.