Commit 2023-02-03 18:30 a4ec43f5
View on Github →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.