Commit 2023-02-16 19:50 740acc0e
View on Github →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.