Stream: new members
Johan Commelin (Nov 04 2019 at 20:05):
Here's a suggestion for mathematicians interested in a follow-up challenge to the nat.nr.game:
- write down a statement in Lean that commuting semisimple endomorphisms/matrices are simultaneously diagonalisable. Think a bit about what is the right generality. In the end, we might want several statements/corollaries.
- post your suggested statement on Zulip, and see what the feedback is.
- solve your self-created level.
- PR the result to mathlib!
Kenny Lau (Nov 04 2019 at 20:08):
while you're at it replace
commuting semisimple endomorphisms/matrices are simultaneously diagonalisable with
Kevin Buzzard (Nov 04 2019 at 20:54):
That's harder though because you'll have to analytically continue the zeta function
Mario Carneiro (Nov 04 2019 at 20:55):
yep, that's definitely the hardest part of proving RH
Kevin Buzzard (Nov 04 2019 at 22:13):
I never said it was the hardest part :D
Last updated: May 11 2021 at 12:15 UTC