Theorem ContinuousLinearMap.spectrum_eq

Modification history

2026-03-10 18:51
Mathlib/Analysis/Normed/Operator/Banach.lean
feat(Analysis/Normed/Operator): prove the Fredholm alternative (#35048) …
Added ContinuousLinearMap.spectrum_eqView on Github →