mathlib3

73530b52 - feat(algebra/algebra/spectrum): prove spectral inclusion for algebra homomorphisms (#12573)

feat(algebra/algebra/spectrum): prove spectral inclusion for algebra homomorphisms (#12573) If `φ : A →ₐ[R] B` is an `R`-algebra homomorphism, then for any `a : A`, `spectrum R (φ a) ⊆ spectrum R a`.