Zulip Chat Archive

Stream: Is there code for X?

Topic: Perron-Frobenius Theorem

Pietro Monticone (Oct 23 2024 at 09:40):

Has the Perron-Frobenius theorem been formalized in Lean?

If so, is it included in Mathlib?

Ruben Van de Velde (Oct 23 2024 at 09:52):

No news since #Is there code for X? > ✔ Perron-Frobenius Theorem, Cauchy's Interlacing Theorem? , I think

Sébastien Gouëzel (Oct 23 2024 at 10:10):

I think @Damien Thomine has a version, but not in Mathlib.

Last updated: May 02 2025 at 03:31 UTC