Theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet

Modification history

2024-02-13 12:46

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

chore(SimpleGraph/IncMatrix): review `Decidable*`/`Fintype _` assumptions (#10445) …

Modified SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet View on Github →

2023-04-05 08:35

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

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

Added SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet View on Github →