mathlib

19deedcc - feat(combinatorics/simple_graph/density): `positivity` extension for `edge_density` (#16640)

feat(combinatorics/simple_graph/density): `positivity` extension for `edge_density` (#16640) Add a `positivity` extension for `rel.edge_density` and `simple_graph.edge_density`. Also golf the file a little using `positivity`.