Commit 2023-03-26 22:26 5ea27f76

chore: forward-port leanprover-community/mathlib#18597 (#2926) This is a forward-port of https://github.com/leanprover-community/mathlib/pull/18597 Some notes:

• This doesn't forward-port the changes to algebra/star/self_adjoint; I plan to re-port this file from scratch after https://github.com/leanprover-community/mathlib/pull/18565 lands. For now, I just add some hacks to keep it compiling.
• It seems that the changes to algebra/periodic were made during porting, see https://github.com/leanprover-community/mathlib4/pull/1963/files/2a6b385f555c37f3eb5e4dd9c113e0a1b5f6b958..578a6252973bcdbd1a6ce4fc0fe2791295cf80e4#r1140354814. So there is nothing to do other than update the SHA.