Skip to content

feat(LinearAlgebra/Eigenspace/Matrix): a scalar is in the spectrum iff it's an eigenvalue#39635

Open
SnirBroshi wants to merge 12 commits into
leanprover-community:masterfrom
SnirBroshi:feature/matrix/mem-spectrum-iff-mulvec
Open

feat(LinearAlgebra/Eigenspace/Matrix): a scalar is in the spectrum iff it's an eigenvalue#39635
SnirBroshi wants to merge 12 commits into
leanprover-community:masterfrom
SnirBroshi:feature/matrix/mem-spectrum-iff-mulvec

remove `isUnit_iff_forall_map_eq_zero`

6bdb864
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jul 5, 2026 in 1m 18s