Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-10 23:42 ef61778b

View on Github →

feat(analysis/normed_space/spectrum): lemmas about spectral radius, spectral mapping and alg_hom_class maps into the base field (#17178)

depends on: #17156

Estimated changes

Modified src/analysis/normed_space/spectrum.lean

added theorem alg_hom.norm_apply_le_self

added theorem alg_hom.norm_apply_le_self_mul_norm_one

added theorem spectrum.exists_nnnorm_eq_spectral_radius

added theorem spectrum.exists_nnnorm_eq_spectral_radius_of_nonempty

added theorem spectrum.map_polynomial_aeval

deleted theorem spectrum.nonempty

added theorem spectrum.spectral_radius_lt_of_forall_lt

added theorem spectrum.spectral_radius_lt_of_forall_lt_of_nonempty

Modified src/analysis/normed_space/star/spectrum.lean