Skip to content

Narrow the two bare import Mathlib to the modules actually used - #40

Merged
leonardoalt merged 1 commit into
mainfrom
narrow-mathlib-imports
Jul 29, 2026
Merged

Narrow the two bare import Mathlib to the modules actually used#40
leonardoalt merged 1 commit into
mainfrom
narrow-mathlib-imports

Commits

Commits on Jul 29, 2026