Commit 2025-11-01 06:18 70c19ec9

View on Github →

feat(Combinatorics/SimpleGraph): a trivial graph has zero degree (#31116) Add helper theorems for #29309

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.degree_eq_one_iff_existsUnique_adj

added theorem SimpleGraph.degree_eq_zero_of_subsingleton

added theorem SimpleGraph.nontrivial_of_degree_ne_zero

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj

deleted theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj

added theorem SimpleGraph.Subgraph.degree_eq_zero_of_subsingleton

added theorem SimpleGraph.Subgraph.degree_of_notMem_verts

added theorem SimpleGraph.Subgraph.degree_pos_iff_exists_adj

added theorem SimpleGraph.Subgraph.nontrivial_verts_of_degree_ne_zero

added theorem SimpleGraph.card_neighborSet_toSubgraph

added theorem SimpleGraph.degree_toSubgraph