Commit 2024-05-16 09:19 93a7eba8

View on Github →

chore(LapMatrix): α -> R (#12868)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

modified def SimpleGraph.degMatrix

modified theorem SimpleGraph.degMatrix_mulVec_apply

modified theorem SimpleGraph.degree_eq_sum_if_adj

modified theorem SimpleGraph.dotProduct_mulVec_degMatrix

modified theorem SimpleGraph.isSymm_degMatrix

modified theorem SimpleGraph.isSymm_lapMatrix

modified def SimpleGraph.lapMatrix

modified theorem SimpleGraph.lapMatrix_mulVec_apply

modified theorem SimpleGraph.lapMatrix_mulVec_const_eq_zero

modified theorem SimpleGraph.lapMatrix_toLinearMap₂'

modified theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj

modified theorem SimpleGraph.posSemidef_lapMatrix