toIcoDiv_sub' — Mathlib

English

If we subtract p from the left argument, the IcoDiv value increases by 1: toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1.

Русский

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

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