move some stuff in Combinatorics.SimpleGraph.LapMatrix?

Stream: mathlib4

[Monica Omar]

While refactoring LinearAlgebra/Matrix/PosDef (deprecating PosSemidef.sqrt to use CFC.sqrt, which as a result meant that we needed to move all these results to a new file in Analysis/Matrix), we found that there are two results in Combinatorics/SimpleGraph/LapMatrix that uses the square root of a matrix, namely: docs#SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj and docs#SimpleGraph.det_lapMatrix_eq_zero.

My question is: should we move these two results to a new file (in, say, Analysis/...)? or is there a workaround to these lemmas without needing the square root?

The imports at the moment on the file within the pr are heavy and get flagged by linter (because it depends on Probability/ConditionalProbability): see #29896

[Monica Omar]

Oh wait, there's also docs#SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable, which is used throughout.
Okay, I don't know what to do. Maybe this whole file needs to be moved?