Skip to content

feat: csum#172

Merged
markusdemedeiros merged 8 commits into
masterfrom
csum
Mar 17, 2026
Merged

feat: csum#172
markusdemedeiros merged 8 commits into
masterfrom
csum

Conversation

@markusdemedeiros
Copy link
Copy Markdown
Collaborator

@markusdemedeiros markusdemedeiros commented Mar 16, 2026

Description

Briefly describe your changes, and link any issues if appropriate.

Fixes # (issue number)

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have updated PORTING.md as appropriate
  • I have added my name to the authors section of any appropriate files

@markusdemedeiros markusdemedeiros merged commit 6373ada into master Mar 17, 2026
1 check passed
@markusdemedeiros markusdemedeiros deleted the csum branch March 17, 2026 19:12
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