mathlib3

feat(combinatorics/graph/multi/basic): Indexed multigraphs

#16100

Open