mathlib3

940d3713 - feat(topology/instances/add_circle): generalize `homeo_Icc_quot` from ℝ to archimedean groups (#17983)

feat(topology/instances/add_circle): generalize `homeo_Icc_quot` from ℝ to archimedean groups (#17983) + Add left/right/two-sided continuity results about `to_Ico/Ioc_mod` and `equiv_Ico`. + Add `tfae_to_Ico_eq_to_Ioc` which states 8 other equivalent conditions for `to_Ico_mod` and `to_Ioc_mod` to agree at a point, from [this comment](https://github.com/leanprover-community/mathlib/pull/17933/files#r1051518394) in #17933. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: loefflerd <d.loeffler.01@cantab.net>