toIcoMod_add_right' — Mathlib

English

In the same setting, shifting the first argument by p increases the result by p: toIcoMod hp (a + p) b = toIcoMod hp a b + p.

Русский

В той же конфигурации сдвиг первого аргумента на p увеличивает результат на p: toIcoMod hp (a + p) b = toIcoMod hp a b + p.

LaTeX

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

Lean4

@[simp]
theorem toIcoMod_add_right' (a b : α) : toIcoMod hp (a + p) b = toIcoMod hp a b + p := by
  simpa only [one_zsmul] using toIcoMod_add_zsmul' hp a b 1

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