mathlib3

ce9af07f - feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966)

feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966) Previously I had use for the operation of reducing a real number to an interval modulo the length of that interval, in proving results about `complex.arg`, and as it was only being used in one place, inlined expressions in terms of `int.fract` and associated proofs where needed. Now I'd like to make further use of that operation, so define actual functions to reduce to an interval (`Ico` or `Ioc`, in an `archimedean` `linear_ordered_add_comm_group`) and set up associated API for those definitions. In the case of a `linear_ordered_field` that is a `floor_ring`, these definitions are proved equal to explicit expressions in terms of `fract` and `floor`. Previous uses for `complex.arg` are updated to illustrate the use of the new API.