English
In a suitable Archimedean ordered additive group, for all a, b ∈ α and m ∈ Z, we have toIocMod hp a (b − m·p) = toIocMod hp a b.
Русский
В подходящей архимедовой упорядоченной аддитивной группе выполняется toIocMod hp a (b − m·p) = toIocMod hp a b.
LaTeX
$$$\forall a,b \in \alpha\,\forall m \in \mathbb{Z},\; toIocMod\ hp\ a\ (b - m\cdot p) = toIocMod\ hp\ a\ b$$$
Lean4
@[simp]
theorem toIocMod_sub_zsmul (a b : α) (m : ℤ) : toIocMod hp a (b - m • p) = toIocMod hp a b := by
rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]