Theorem Subalgebra.spectrum_eq_of_isPreconnected_compl

Modification history

2024-08-16 23:11
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
feat: better proof of spectral permanence (#15603) …
Added Subalgebra.spectrum_eq_of_isPreconnected_complView on Github →