toIocMod_add_left' — Mathlib

English

Shifting the left argument by p yields p plus toIocMod hp a b: toIocMod hp (p + a) b = p + toIocMod hp a b.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toIocMod_add_left' (a b : α) : toIocMod hp (p + a) b = p + toIocMod hp a b := by
  rw [add_comm, toIocMod_add_right', add_comm]

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