Commit 2024-10-15 14:06 b71a4970
View on Github →chore: move Init.Algebra.Classes and its remaining dependencies to Deprecated (#17769)
The results in this file have been deprecated for a while and none seem to be used in Mathlib except for other deprecated results that aren't used either. So let's move everything to the Deprecated folder in order to empty out the Init folder.