Skip to content

chore: PRd WithRPowDist to Mathlib#11

Merged
urkud merged 2 commits intomainfrom
pr-33114
Dec 20, 2025
Merged

chore: PRd WithRPowDist to Mathlib#11
urkud merged 2 commits intomainfrom
pr-33114

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 00:57
@urkud urkud merged commit 834d5b4 into main Dec 20, 2025
1 check passed
@urkud urkud deleted the pr-33114 branch December 20, 2025 01:09
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