toIocDiv_add_right' — Mathlib

English

For hp > 0 and a, b ∈ α, shifting the left argument by p decreases the value by 1: toIocDiv hp (a + p) b = toIocDiv hp a b − 1.

Русский

Для hp > 0 и любых a, b ∈ α сдвиг левого аргумента на 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_right' (a b : α) : toIocDiv hp (a + p) b = toIocDiv hp a b - 1 := by
  simpa only [one_zsmul] using toIocDiv_add_zsmul' hp a b 1

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