Commit 2023-08-20 20:55 dcc92db9

View on Github →

feat: matrix equality of strongly regular graphs (#6507)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added def SimpleGraph.walkLengthTwoEquivCommonNeighbors

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

added theorem SimpleGraph.IsSRGWith.matrix_eq