toIocDiv_add_zsmul — Mathlib

English

Same as the previous, illustrating the additive shift in the argument of toIcoDiv by m p.

Русский

То же самое, иллюстрирующее приращение аргумента toIcoDiv на m p.

LaTeX

$$$$\text{toIcoDiv}(hp, a, b + m p) = \text{toIcoDiv}(hp, a, b) + m$$$$

Lean4

@[simp]
theorem toIocDiv_add_zsmul (a b : α) (m : ℤ) : toIocDiv hp a (b + m • p) = toIocDiv hp a b + m :=
  toIocDiv_eq_of_sub_zsmul_mem_Ioc hp <| by
    simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIocDiv_zsmul_mem_Ioc hp a b

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