refactor: redefine spectralRadius in terms of quasispectrum - #42753

refactor: redefine spectralRadius in terms of quasispectrum#42753

j-loreaux wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

j-loreaux:quasi-spectralRadiusj-loreaux/mathlib4:quasi-spectralRadiusCopy head branch name to clipboard