feat(Combinatorics/SimpleGraph/LapMatrix): 0 is always an eigenvalue#39627

Open

SnirBroshi wants to merge 10 commits into

leanprover-community:masterfrom

SnirBroshi:feature/simple-graph/zero-eigenvalue-lap-matrix

Commits on May 21, 2026

the determinant of the Laplacian is zero even for non-domains
SnirBroshi
committed
Merge branch 'master' into feature/simple-graph/zero-eigenvalue-lap-matrix
SnirBroshi
authored
`not_isUnit_lapMatrix` is now trivial given the new `det_lapMatrix_eq_zero`
SnirBroshi
committed