Perron-Frobenius Theorem, Cauchy's Interlacing Theorem?

Stream: Is there code for X?

[leafGecko]

^

[Scott Morrison]

No, we don't have either of these, and both would be great additions to mathlib.

[leafGecko]

I tried greping through current mathlib for "Frobenius" / "Interlacing", but no result. I am still not quite sure as maybe someone just didn't put the name in comment ... Is there a reliable way of finding theorems?

[Scott Morrison]

Grep, ask here, and library_search.

[Scott Morrison]

If you see "theorems with names", but the names aren't in doc-strings in mathlib, we would welcome a PR improving the doc-strings!

[leafGecko]

I see. Thanks!