mathlib
541a1a02 - refactor(combinatorics/simple_graph/{basic,degree_sum}): move darts from degree_sum to basic (#12195)

Commit
3 years ago
refactor(combinatorics/simple_graph/{basic,degree_sum}): move darts from degree_sum to basic (#12195) This also changes `simple_graph.dart` to extend `prod`, so that darts are even closer to being an ordered pair. Since this touches the module docstrings, they are updated to use fully qualified names.
Author
Parents
Loading