Theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectral_radius
Modification history
2022-10-10 20:56
src/analysis/normed_space/spectrum.lean
refactor(analysis/normed_space/spectrum): remove `norm_one_class` hypotheses (#16891) …
Modified spectrum.pow_norm_pow_one_div_tendsto_nhds_spectral_radiusView on Github →