spectrum): lemmas about spectral radius, spectral mapping and `alg_hom_class` maps into the base field (#17178)

Commit

3 years ago

feat(analysis/normed_space/spectrum): lemmas about spectral radius, spectral mapping and `alg_hom_class` maps into the base field (#17178) - [x] depends on: #17156

Author

j-loreaux

Parents

13bc7a20

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

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