mathlib3

213b0cff - feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743)

feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743) This also provides us with the same instance for `real.angle`. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Mauricio Collares <mauricio@collares.org>