Mathlib v3 is deprecated. Go to Mathlib v4

Theorem spectrum.spectral_radius.of_subsingleton

Modification history

2022-10-10 20:56

src/analysis/normed_space/spectrum.lean

refactor(analysis/normed_space/spectrum): remove `norm_one_class` hypotheses (#16891) …

Added spectrum.spectral_radius.of_subsingleton View on Github →