mathlib

a4ec43f5 - refactor(combinatorics/simple_graph/density): Generalize to arbitrary ordered fields (#18370)

refactor(combinatorics/simple_graph/density): Generalize to arbitrary ordered fields (#18370) I originally thought making graph densities `ℚ`-valued would work best, but I now need it to be a real and it turns out to be more pain than anything.