mathlib3

740acc0e - feat(algebra/order): Unions of interval translates by ℤ (#18427)

feat(algebra/order): Unions of interval translates by ℤ (#18427) Write a linearly ordered abelian group as a union of pairwise disjoint intervals `⋃ (n : ℤ), Ioc (a + n • b) (a + (n + 1) • b)` (in multiple variations). Split off from #18425, which in turn was split from #18392.