Commit 2026-06-04 18:51 3a31d5b7

View on Github →

feat(Combinatorics/SimpleGraph/Star): define star graphs (#38027) Add a new definition starGraph and several key lemmas. Star graphs are a trivial class of tree, often used in constructive proofs regarding trees. An example use case is shown in #38334.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Star.lean

added theorem SimpleGraph.connected_starGraph

added theorem SimpleGraph.degree_starGraph_center

added theorem SimpleGraph.degree_starGraph_of_ne_center

added theorem SimpleGraph.isAcyclic_starGraph

added theorem SimpleGraph.isTree_starGraph

added def SimpleGraph.starGraph

added theorem SimpleGraph.starGraph_adj

added theorem SimpleGraph.starGraph_adj_center_iff

added theorem SimpleGraph.starGraph_center_adj'

added theorem SimpleGraph.starGraph_center_adj