Skip to content

chore: update Mathlib#12

Merged
urkud merged 1 commit intomainfrom
update-mathlib
Dec 20, 2025
Merged

chore: update Mathlib#12
urkud merged 1 commit intomainfrom
update-mathlib

Conversation

@urkud
Copy link
Copy Markdown
Owner

@urkud urkud commented Dec 20, 2025

No description provided.

@urkud urkud enabled auto-merge (squash) December 20, 2025 08:38
@urkud urkud merged commit 074c04c into main Dec 20, 2025
1 check passed
@urkud urkud deleted the update-mathlib branch December 20, 2025 08:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant