Theorem SimpleGraph.posSemidef_lapMatrix

Modification history

2024-07-07 19:14
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
chore (BigOperators.Finsupp): avoid importing `Order.BigOperators.Ring.Finset` (#14336) …
Modified SimpleGraph.posSemidef_lapMatrixView on Github →
2024-05-16 09:19
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
chore(LapMatrix): `α` -> `R` (#12868)
Modified SimpleGraph.posSemidef_lapMatrixView on Github →
2024-04-05 15:59
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
feat: make `StarOrderedRing` a mixin (#11872) …
Modified SimpleGraph.posSemidef_lapMatrixView on Github →
2024-02-28 12:44
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
feat: Laplacian matrix of a simple graph (#8594) …
Added SimpleGraph.posSemidef_lapMatrixView on Github →