mathlib3

6ac7c18d - feat(combinatorics/simple_graph/density): Edge density (#12431)

feat(combinatorics/simple_graph/density): Edge density (#12431) Define the number and density of edges of a relation and of a simple graph between two finsets. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>