Commit 2024-09-08 13:32 3fecb249

View on Github →

feat(Combinatorics/SimpleGraph): define the line graph of a simple graph (#16276) This is pretty bare-bones for now.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/LineGraph.lean

added def SimpleGraph.lineGraph

added theorem SimpleGraph.lineGraph_adj_iff_exists

added theorem SimpleGraph.lineGraph_bot