Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-23 16:58 6f1ad825

View on Github →

chore(algebra/algebra/spectrum): generalize some spectrum results from alg_hom to alg_hom_class (#16177)

depends on: #16178

Estimated changes

Modified src/algebra/algebra/spectrum.lean

modified theorem alg_hom.apply_mem_spectrum

modified theorem alg_hom.mem_resolvent_set_apply

modified theorem alg_hom.spectrum_apply_subset

Modified src/analysis/normed_space/spectrum.lean

added theorem alg_hom.coe_to_continuous_linear_map

deleted theorem alg_hom.continuous

modified def alg_hom.to_continuous_linear_map

Modified src/topology/algebra/module/character_space.lean