-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(combinatorics/simple_graph/density): Edge density #12431
Conversation
Looks reasonable to me, and I didn't notice anything that's in need of improvement. One slight inaccuracy is that, technically, interedges are darts -- if the expectation is that the main use case is that the two vertex sets are disjoint, I think this is OK. You might consider making things be dart-valued, but I suggest only doing that if in the short term that would be useful. (Justification: if this ever changes in the future, it should be an easy refactor.) @awainverse Would you mind taking a look at the relations part of this PR? Would you have a home for it that you'd prefer over |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall, this looks like good design.
Thanks 🎉 bors merge |
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>
Pull request successfully merged into master. Build succeeded: |
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
From SRL