mathlib

075ff371 - refactor(algebra/order*): move files about ordered algebraic structures into subfolder (#9024)

refactor(algebra/order*): move files about ordered algebraic structures into subfolder (#9024) There were many files named `algebra/order_*.lean`. There are also `algebra.{module,algebra}.ordered`. The latter are Prop-valued mixins. This refactor moves the data typeclasses into their own subfolder. That should help facilitate organizing further refactoring to provide the full gamut of the order x algebra hierarchy.