mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(Algebra/BigOperators): add missing deprecation dates

Open grunweg opened this issue 1 year ago • 6 comments
trafficstars

One additivised lemma was missing a deprecation.

Open in Gitpod

grunweg avatar May 02 '24 14:05 grunweg

awaiting-review

grunweg avatar May 07 '24 09:05 grunweg

awaiting-review

grunweg avatar May 11 '24 14:05 grunweg

bors merge

kim-em avatar May 16 '24 12:05 kim-em

Build failed:

mathlib-bors[bot] avatar May 16 '24 13:05 mathlib-bors[bot]

Please fix the CI error, and then send to bors.

bors d+

kim-em avatar May 21 '24 06:05 kim-em

:v: grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-bors[bot] avatar May 21 '24 06:05 mathlib-bors[bot]

bors r+

grunweg avatar May 24 '24 20:05 grunweg

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 24 '24 21:05 mathlib-bors[bot]