Skip to content

chore: remove Mathlib namespace from library note links#765

Merged
bryangingechen merged 1 commit intoleanprover-community:lean4from
chenson2018:library-note-upstream
Dec 13, 2025
Merged

chore: remove Mathlib namespace from library note links#765
bryangingechen merged 1 commit intoleanprover-community:lean4from
chenson2018:library-note-upstream

Commits

Commits on Dec 13, 2025