[Merged by Bors] - feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball)#36443
Closed
Fieldnote-Echo wants to merge 8 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball)#36443Fieldnote-Echo wants to merge 8 commits intoleanprover-community:masterfrom
Fieldnote-Echo wants to merge 8 commits intoleanprover-community:masterfrom
Commits
Commits on Apr 19, 2026
- committed
- committed
- committed
- committed
- andcommitted
- andcommitted
- andcommitted
- committed
