Skip to content

[Merged by Bors] - chore: redefine DivInvMonoid.zpow_succ' field #36931

[Merged by Bors] - chore: redefine DivInvMonoid.zpow_succ' field

[Merged by Bors] - chore: redefine DivInvMonoid.zpow_succ' field #36931

Triggered via pull request October 9, 2024 15:05
Status Success
Total duration 12s
Artifacts

label_new_contributor.yml

on: pull_request
label-and-report-new-contributor
3s
label-and-report-new-contributor
Fit to window
Zoom out
Zoom in