Commit 2024-04-25 07:11 ffaeb65b

View on Github →

chore(Combinatorics/SimpleGraph): Generalize few lemmas in AdjMatrix to NonAssocSemiring α (#12413) Generalize some lemmas from ℕ, Ring α, and Semiring α, to NonAssocSemiring α.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

modified theorem SimpleGraph.adjMatrix_mulVec_const_apply

modified theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular

modified theorem SimpleGraph.dotProduct_mulVec_adjMatrix

modified theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes