toIcoDiv_add_left — Mathlib

English

For hp > 0, adding p to the right argument yields: toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1.

Русский

Для hp > 0 добавление p к правому аргументу даёт: toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1.

LaTeX

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

Lean4

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

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