toIcoMod_add_left' — Mathlib

English

If you shift the left argument by p, you obtain p plus toIocMod hp a b: toIcoMod hp (p + a) b = p + toIocMod hp a b.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toIcoMod_add_left' (a b : α) : toIcoMod hp (p + a) b = p + toIcoMod hp a b := by
  rw [add_comm, toIcoMod_add_right', add_comm]

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