Theorem Module.End.eigenspace_mem_invtSubmodule

Modification history

2026-03-19 02:11
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
feat(Analysis/InnerProductSpace/Spectrum): eigenspaces of a compact selfadjoint operator exhaust the Hilbert space (#36520) …
Added Module.End.eigenspace_mem_invtSubmoduleView on Github →