mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

chore(Algebra): add missing deprecation dates

Open grunweg opened this issue 1 year ago • 1 comments


  • [ ] depends on: #12597

Open in Gitpod

grunweg avatar May 02 '24 14:05 grunweg

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#12597~~ By Dependent Issues (🤖). Happy coding!

Thanks! :tada: bors merge

urkud avatar May 26 '24 06:05 urkud

Thanks for the fast review!

grunweg avatar May 26 '24 06:05 grunweg

Pull request successfully merged into master.

Build succeeded:

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