Commit 2023-02-07 20:30 10d1590a
View on Github →fix: added missing theorems in Algebra.Order.Archimedean (#2150) exists_unique_sub_zsmul_mem_Ico and exists_unique_sub_zsmul_mem_Ioc did not seem to get ported for some reason. They're used in Algebra/Order/ToIntervalMod, so let's fix this!