toIcoDiv_add_left' — Mathlib

English

If you shift the left argument by p, the result decreases by 1: toIcoDiv hp (p + a) b = toIcoDiv hp a b − 1.

Русский

Если сдвинуть левый аргумент на p, результат уменьшается на 1: toIcoDiv hp (p + a) b = toIcoDiv hp a b − 1.

LaTeX

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

Lean4

@[simp]
theorem toIcoDiv_add_left' (a b : α) : toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1 := by
  rw [add_comm, toIcoDiv_add_right']

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