toIocDiv_add_left' — Mathlib

English

Shifting the left argument by p decreases the value by 1: toIocDiv hp (p + a) b = toIocDiv hp a b − 1.

Русский

Сдвиг левого аргумента на p уменьшает значение на 1: toIocDiv hp (p + a) b = toIocDiv hp a b − 1.

LaTeX

$$$\operatorname{toIocDiv}\\_{hp}(p + a, b) = \operatorname{toIocDiv}\\_{hp}(a, b) - 1$$$

Lean4

@[simp]
theorem toIocDiv_add_left' (a b : α) : toIocDiv hp (p + a) b = toIocDiv hp a b - 1 := by
  rw [add_comm, toIocDiv_add_right']

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