Commit 2021-10-18 23:50 98d07d31

refactor(algebra/order): replace typeclasses with constructors (#9725) This RFC suggests removing some unused classes for the ordered algebra hierarchy, replacing them with constructors We have nonneg_add_comm_group extends add_comm_group, and an instance from this to ordered_add_comm_group. The intention is to be able to construct an ordered_add_comm_group by specifying its positive cone, rather than directly its order. There are then nonneg_ring and linear_nonneg_ring, similarly. (None of these are actually used later in mathlib at this point.)