## Stream: new members

### Topic: commuting endomorphisms simultaneously diagonalisable

#### 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:

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.
4. 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 Riemann's hypothesis

#### 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