toIocDiv_add_right — Mathlib

English

Let hp be as above. For any a, b ∈ α, adding p to the second argument increases by 1: toIocDiv hp a (b + p) = toIocDiv hp a b + 1.

Русский

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

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