Commit 2024-05-27 18:18 b32641fd

View on Github →

chore(AdjMatrix): generalize a lemma (#12867) Slightly generalize dotProduct_mulVec_adjMatrix. The old version is G.dotProduct_mulVec_adjMatrix vec vec.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

modified theorem SimpleGraph.dotProduct_mulVec_adjMatrix