Theorem SimpleGraph.fromEdgeSet_not_isDiag

Modification history

2025-12-01 17:55
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat(Combinatorics/SimpleGraph): use `Sym2.diagSet` instead of explicit sets (#32255)
Modified SimpleGraph.fromEdgeSet_not_isDiagView on Github →
2025-11-13 20:22
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat: the graph made of all non-diag edges is complete (#31443)
Added SimpleGraph.fromEdgeSet_not_isDiagView on Github →