toIcoDiv_add_zsmul — Mathlib

English

For all a, b and m ∈ ℤ, toIcoDiv(hp, a, b + m p) = toIcoDiv(hp, a, b) + m.

Русский

Для любых a, b и m ∈ ℤ выполняется toIcoDiv(hp, a, b + m p) = toIcoDiv(hp, a, b) + m.

LaTeX

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

Lean4

@[simp]
theorem toIcoDiv_add_zsmul (a b : α) (m : ℤ) : toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + m :=
  toIcoDiv_eq_of_sub_zsmul_mem_Ico hp <| by
    simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIcoDiv_zsmul_mem_Ico hp a b

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