mathlib3

905871f4 - feat(analysis/normed_space/spectrum): an algebra homomorphism into the base field is bounded (#11494)

feat(analysis/normed_space/spectrum): an algebra homomorphism into the base field is bounded (#11494) We prove basic facts about `φ : A →ₐ[𝕜] 𝕜` when `A` is a Banach algebra, namely that `φ` maps elements of `A` to their spectrum, and that `φ` is bounded. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>