Deprecated aliases can be dumped here if they are no longer used in Mathlib, to avoid needing their imports if they are otherwise unnecessary.