Commit 2026-09-05 14:32 4cbb42e7

View on Github →

feat(Combinatorics/SimpleGraph/Finite): the Fintype instance for incidenceSet doesn't need DecidableEq (#41713) Now it only requires Fintype (G.neighborSet v). This caused incidenceFinset and theorems about it to complain that DecidableEq is unused, so I changed incidenceFinset to require Fintype (G.incidenceSet v) and fixed the theorems. Theorems that require a finite neighborSet can avoid this.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.card_incidenceFinset_eq_degree

modified theorem SimpleGraph.card_incidenceSet_eq_degree

modified theorem SimpleGraph.coe_incidenceFinset

modified theorem SimpleGraph.disjoint_incidenceFinset_of_disjoint

modified def SimpleGraph.incidenceFinset

modified theorem SimpleGraph.incidenceFinset_subset

modified theorem SimpleGraph.mem_incidenceFinset