mathlib3

feat(combinatorics/simple_graph): Locally linear graphs

#19201

Closed