[Merged by Bors] - chore: remove declarations deprecated between 2021-04-15 and 2025-10-15#38057
Closed
mathlib-nolints[bot] wants to merge 6 commits intomasterfrom
Closed
[Merged by Bors] - chore: remove declarations deprecated between 2021-04-15 and 2025-10-15#38057mathlib-nolints[bot] wants to merge 6 commits intomasterfrom
mathlib-nolints[bot] wants to merge 6 commits intomasterfrom
![mathlib-nolints[bot]](https://avatars.githubusercontent.com/u/41703605?v=4&size=32){kind=avatar}
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=32){kind=avatar}
