Mathlib Changelog
v4
Changelog
About
Github
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