toIocMod_add_right' — Mathlib

English

Shifting the left argument by p increases the right-hand side by p: toIocMod hp (a + p) b = toIocMod hp a b + p.

Русский

Сдвиг левого аргумента на p увеличивает правую часть на p: toIocMod hp (a + p) b = toIocMod hp a b + p.

LaTeX

$$$\forall a,b \in \alpha,\; toIocMod\ hp\ (a + p)\ b = toIocMod\ hp\ a\ b + p$$$

Lean4

@[simp]
theorem toIocMod_add_right' (a b : α) : toIocMod hp (a + p) b = toIocMod hp a b + p := by
  simpa only [one_zsmul] using toIocMod_add_zsmul' hp a b 1

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