[Merged by Bors] - feat: Number of edges of a tree #5918
Conversation
Port/review of mathlib#18638 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
kmill
added
awaiting-review
| lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) : | ||
| Finset.card G.edgeFinset + 1 = Fintype.card V := by |
There was a problem hiding this comment.
I'm a bit sad to see Fintype and Finset.card instead of Finite and Nat.card but poking around the graph theory library I see this is consistent with the rest.
What view do @b-mehta @YaelDillies @kmill @bottine have on refactoring to the classical world?
There was a problem hiding this comment.
@ocfnash The graph theory library pre-dates Finite (and you might notice that I'm the author of Finite, so you might be able to guess my general thoughts 😉). I hope eventually we can use Finite, but that'll take switching from things like Finset.sum to suitable Set counterparts. Any thoughts of refactoring had been put on hold due to the port.
There was a problem hiding this comment.
finset works great for the graph theory library. I don't think there's any switching to be done, but I agree that we should have nicer ways to say "This graph is finite" than spelling out all the fintype instaces.
leanprover-community-mathlib4-bot
added
ready-to-merge
Port/review of [mathlib#18638](leanprover-community/mathlib#18638) directly to Mathlib4. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Port/review of [mathlib#18638](leanprover-community/mathlib#18638) directly to Mathlib4. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Port/review of [mathlib#18638](leanprover-community/mathlib#18638) directly to Mathlib4. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Port/review of [mathlib#18638](leanprover-community/mathlib#18638) directly to Mathlib4. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Port/review of [mathlib#18638](leanprover-community/mathlib#18638) directly to Mathlib4. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Port/review of mathlib#18638 directly to Mathlib4.
Co-authored-by: Yaël Dillies yael.dillies@gmail.com
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com