toIocDiv_sub' — Mathlib

English

Subtracting p from the left argument yields the same pattern with +1: toIocDiv hp (a - p) b = toIocDiv hp a b + 1.

Русский

Вычитание p из левого аргумента сохраняет закономерность: 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_sub' (a b : α) : toIocDiv hp (a - p) b = toIocDiv hp a b + 1 := by
  simpa only [one_zsmul] using toIocDiv_sub_zsmul' hp a b 1

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