Commit 2024-02-13 12:46 9db90fd7

View on Github →

chore(SimpleGraph/IncMatrix): review Decidable*/Fintype _ assumptions (#10445) Drop unneeded assumptions, modify other assumptions to match exactly what's required to formulate the theorems.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

modified theorem SimpleGraph.incMatrix_mul_transpose

modified theorem SimpleGraph.incMatrix_mul_transpose_diag

modified theorem SimpleGraph.incMatrix_transpose_mul_diag

modified theorem SimpleGraph.sum_incMatrix_apply

modified theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet

modified theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet