mathlib3
[Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s
#19168

Closed

[Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s #19168

ericrbg wants to merge 1 commit into master from soy-un-burro

chore(*/centralizer): add forgotten `to_additive`s

55d712ee

ericrbg added awaiting-review

ericrbg added awaiting-CI

ericrbg added modifies-synchronized-file

urkud commented on 2023-06-09

github-actions removed awaiting-CI

eric-wieser approved these changes on 2023-06-09

leanprover-community-bot-assistant added ready-to-merge

leanprover-community-bot-assistant removed awaiting-review

bors changed the title ~~chore(*/centralizer): add forgotten `to_additive`s~~ [Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s 3 years ago

bors closed this 3 years ago

bors deleted the soy-un-burro branch 3 years ago

Reviewers

eric-wieser

urkud

Assignees

No one assigned

Labels

ready-to-merge modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s #19168 Closed

[Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s #19168

mathlib3
[Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s
#19168

Closed