Skip to content
move-decls (comment)

[Merged by Bors] - feat(Algebra/Order/Ring/WithTop): add generalised and specialised power of top #5978

Sign in to view logs

[Merged by Bors] - feat(Algebra/Order/Ring/WithTop): add generalised and specialised power of top

[Merged by Bors] - feat(Algebra/Order/Ring/WithTop): add generalised and specialised power of top #5978

Triggered via issue June 23, 2024 07:01
@sgouezelsgouezel
commented on #14019 92377b4
Status Skipped
Total duration 2s
Artifacts –

move_decl_comment.yml

on: issue_comment
move-decls-add-comment
0s
move-decls-add-comment
Fit to window
Zoom out
Zoom in