Commit 2024-02-07 03:57 bbbf0378

View on Github →

refactor: split out graph darts (#10312) Continuation from #10123. Combinatorics.SimpleGraph.Basic is now under 1000 lines.

Estimated changes

deleted theorem SimpleGraph.Dart.edge_mem
deleted theorem SimpleGraph.Dart.edge_mk
deleted theorem SimpleGraph.Dart.ext
deleted theorem SimpleGraph.Dart.ext_iff
deleted theorem SimpleGraph.Dart.symm_mk
deleted theorem SimpleGraph.Dart.symm_ne
deleted structure SimpleGraph.Dart
deleted def SimpleGraph.DartAdj
modified def SimpleGraph.fromRel
added theorem SimpleGraph.Dart.ext
added structure SimpleGraph.Dart