toIocDiv_add_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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