Theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular

Modification history

2024-04-25 07:11

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

chore(Combinatorics/SimpleGraph): Generalize few lemmas in `AdjMatrix` to `NonAssocSemiring α` (#12413) …

Modified SimpleGraph.adjMatrix_mulVec_const_apply_of_regular View on Github →

2023-04-05 14:36

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

feat: port Combinatorics.SimpleGraph.AdjMatrix (#3287)

Added SimpleGraph.adjMatrix_mulVec_const_apply_of_regular View on Github →