Theorem SimpleGraph.coe_incidenceFinset

Modification history

2026-09-05 14:32

Mathlib/Combinatorics/SimpleGraph/Finite.lean

feat(Combinatorics/SimpleGraph/Finite): the `Fintype` instance for `incidenceSet` doesn't need `DecidableEq` (#41713) …

Modified SimpleGraph.coe_incidenceFinset View on Github →

2026-01-24 00:25

Mathlib/Combinatorics/SimpleGraph/Finite.lean

refactor(SimpleGraph/Finite): turn `edgeFinset` into a `def` (#28821) …

Added SimpleGraph.coe_incidenceFinset View on Github →