2026-03-19 02:11
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
feat(Analysis/InnerProductSpace/Spectrum): eigenspaces of a compact selfadjoint operator exhaust the Hilbert space (#36520) …
Added ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero