commuting endomorphisms simultaneously diagonalisable

Stream: new members

[Johan Commelin]

Here's a suggestion for mathematicians interested in a follow-up challenge to the nat.nr.game:

1. 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.
2. post your suggested statement on Zulip, and see what the feedback is.
3. solve your self-created level.
4. PR the result to mathlib!

[Kenny Lau]

while you're at it replace commuting semisimple endomorphisms/matrices are simultaneously diagonalisable with Riemann's hypothesis

[Kevin Buzzard]

That's harder though because you'll have to analytically continue the zeta function

[Mario Carneiro]

yep, that's definitely the hardest part of proving RH

[Kevin Buzzard]

I never said it was the hardest part :D