Theorem SimpleGraph.isHermitian_adjMatrix

Modification history

2026-03-18 22:07

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

feat(Combinatorics/SimpleGraph/LapMatrix): {`adjMatrix`/`degMatrix`/`lapMatrix`} are Hermitian (#36335) …

Added SimpleGraph.isHermitian_adjMatrix View on Github →