grunweg

feat: lint `attribute [instance] instName in`

2

Contrary to what users would expect, this defines a global instance. This linter would have caught #13144 and #13170. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ConcreteCategory.2EinstFunLike.20became.20a.20.20global.20instance) Co-authored by: @adomani --- [](https://gitpod.io/from-referrer/)

chore(Algebra): add missing deprecation dates

1

--- - [ ] depends on: #12597 [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

TODO: wait until #12598 has landed (to simplify the diff); use since syntax. --- [](https://gitpod.io/from-referrer/)

This is not exhaustive, but covers ~100 declarations. --- Commits can be reviewed individually. [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

Tracking issue: configuration for linters and further CI checks

3

Currently, the project does not set up any configuration for running linters etc. I think it should do so, depending what the goal of the project is. Let's go through...

Currently, this also removes a number of previously present tags of articles; that part obviously needs to be reverted. Help with that (and with tagging the new articles) is very...

- depends on: mathlib4#30413 - further use will need - a fix in the elaborators: if E is a real inner product space, we don't find the trivial model yet...