toIocDiv_sub — Mathlib

English

For hp > 0, subtracting p from the right argument decreases the IocDiv value by 1: toIocDiv hp a (b - p) = toIocDiv hp a b - 1.

Русский

Для hp > 0 вычитание p из правого аргумента уменьшает IocDiv на 1: toIocDiv hp a (b - p) = toIocDiv hp a b − 1.

LaTeX

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

Lean4

@[simp]
theorem toIocDiv_sub (a b : α) : toIocDiv hp a (b - p) = toIocDiv hp a b - 1 := by
  simpa only [one_zsmul] using toIocDiv_sub_zsmul hp a b 1

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