Commit 2026-08-27 20:56 baa74fbf

View on Github →

feat(Combinatorics/SimpleGraph/LapMatrix): 0 is always an eigenvalue (#39627) and the determinant is always zero, plus a few other small lemmas.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

added theorem SimpleGraph.IsIsolated.not_isUnit_degMatrix

added theorem SimpleGraph.IsRegularOfDegree.degMatrix_eq

added theorem SimpleGraph.IsRegularOfDegree.mem_spectrum_adjMatrix

added theorem SimpleGraph.degMatrix_bot

added theorem SimpleGraph.degMatrix_top

modified theorem SimpleGraph.det_lapMatrix_eq_zero

added theorem SimpleGraph.lapMatrix_bot

added theorem SimpleGraph.lapMatrix_mulVec_apply'

deleted theorem SimpleGraph.lapMatrix_mulVec_const_eq_zero

added theorem SimpleGraph.lapMatrix_mulVec_one_eq_zero

modified theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable

added theorem SimpleGraph.lapMatrix_top

added theorem SimpleGraph.not_isUnit_lapMatrix

added theorem SimpleGraph.zero_mem_spectrum_lapMatrix