Skip to content

docs: mark SimpleGraph.ball upstreamed in Mathlib #36443#14

Merged
Navi Bot (project-navi-bot) merged 1 commit into
mainfrom
docs/simplegraph-ball-upstreamed
May 13, 2026
Merged

docs: mark SimpleGraph.ball upstreamed in Mathlib #36443#14
Navi Bot (project-navi-bot) merged 1 commit into
mainfrom
docs/simplegraph-ball-upstreamed

Commits

Commits on May 13, 2026