toIocMod_add_zsmul' — Mathlib

English

For any a, b and integer m, toIocMod hp (m p + a) b = m p + toIocMod hp a b.

Русский

Для любых a, b и целого m: toIocMod hp (m p + a) b = m p + toIocMod hp a b.

LaTeX

$$$\operatorname{toIocMod}\\_{hp}(m \cdot p + a, b) = m \cdot p + \operatorname{toIocMod}\\_{hp}(a, b)$$$

Lean4

@[simp]
theorem toIocMod_add_zsmul' (a b : α) (m : ℤ) : toIocMod hp (a + m • p) b = toIocMod hp a b + m • p := by
  simp only [toIocMod, toIocDiv_add_zsmul', sub_smul, sub_add]

Похожие утверждения