Commit 2023-01-14 12:14 a0ed43b3
View on Github →fix(algebra/order/to_interval_mod): align to_Ico_div with regular division (#18105)
The previous definition of to_Ico_div and to_Ico_mod had x = to_Ico_mod a hb x - to_Ico_div a hb x • b; but the usual convention for div and mod is x = x / b + x % b • b.
This change flips the sign, and adjust all the lemmas accordingly.
As a result, we now have the more natural to_Ico_div a hb x = ⌊(x - a) / b⌋ instead of the previous to_Ico_div a hb x = -⌊(x - a) / b⌋.
This also changes
def mem_Ioo_mod (b x : α) : Prop :=
-∃ z : ℤ, x + z • b ∈ set.Ioo a (a + b)
+∃ z : ℤ, x - z • b ∈ set.Ioo a (a + b)
even though the two are equivalent; because this means that z corresponds to to_Ico_div .