Zulip Chat Archive

Stream: new members

Topic: commuting endomorphisms simultaneously diagonalisable


view this post on Zulip 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.
  3. solve your self-created level.
  4. PR the result to mathlib!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 04 2019 at 20:54):

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

view this post on Zulip Mario Carneiro (Nov 04 2019 at 20:55):

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

view this post on Zulip 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