mathlib3

05ee42cf - feat(order/circular): define circular orders (#9413)

feat(order/circular): define circular orders (#9413) A circular order is the way to formalize positions on a circle. This is very foundational, as a good lot of the order-algebra-topology hierarchy has a circular analog.