Skip to content

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
Open

feat(Combinatorics/SimpleGraph/LapMatrix): 0 is always an eigenvalue#39627
SnirBroshi wants to merge 10 commits into
leanprover-community:masterfrom
SnirBroshi:feature/simple-graph/zero-eigenvalue-lap-matrix

`not_isUnit_lapMatrix` is now trivial given the new `det_lapMatrix_eq…

7e35d51
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded May 21, 2026 in 1m 19s