Theorem SimpleGraph.Subgraph.nontrivial_verts_of_degree_ne_zero

Modification history

2025-11-01 06:18
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
feat(Combinatorics/SimpleGraph): a trivial graph has zero degree (#31116) …
Added SimpleGraph.Subgraph.nontrivial_verts_of_degree_ne_zeroView on Github →