Commit 2023-04-05 08:35 9ce81ec6

View on Github →

feat: port Combinatorics.SimpleGraph.IncMatrix (#3274)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

added theorem SimpleGraph.incMatrix_apply'

added theorem SimpleGraph.incMatrix_apply

added theorem SimpleGraph.incMatrix_apply_eq_one_iff

added theorem SimpleGraph.incMatrix_apply_eq_zero_iff

added theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply

added theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adj

added theorem SimpleGraph.incMatrix_mul_transpose

added theorem SimpleGraph.incMatrix_mul_transpose_apply_of_adj

added theorem SimpleGraph.incMatrix_mul_transpose_diag

added theorem SimpleGraph.incMatrix_of_mem_incidenceSet

added theorem SimpleGraph.incMatrix_of_not_mem_incidenceSet

added theorem SimpleGraph.incMatrix_transpose_mul_diag

added theorem SimpleGraph.sum_incMatrix_apply

added theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet

added theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet