Skip to content

chore: bump mathlib to 8819c75, fix breaking changes - #225

Closed
github-actions[bot] wants to merge 1 commit into
mainfrom
bump-mathlib/fix-8819c75
Closed

github-actions[bot] wants to merge 1 commit into
mainfrom
bump-mathlib/fix-8819c75

Commits

Commits on Aug 26, 2026