Theorem Module.End.HasEigenvalue.mem_spectrum

Modification history

2024-05-02 19:23
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
feat: enable dot notation for `HasEigenvalue` and the spectrum (#12580)
Added Module.End.HasEigenvalue.mem_spectrumView on Github →