toIcoDiv_sub — Mathlib

English

For hp > 0, subtracting p from the second argument reduces the IcoDiv value by 1: toIcoDiv hp a (b - p) = toIcoDiv hp a b − 1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toIcoDiv_sub (a b : α) : toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1 := by
  simpa only [one_zsmul] using toIcoDiv_sub_zsmul hp a b 1

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