toIcoDiv_add_zsmul' — Mathlib

English

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

Русский

Для hp, a, b ∈ α и m ∈ ℤ: toIcoDiv(hp, a + m p, b) = toIcoDiv(hp, a, b) − m.

LaTeX

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

Lean4

@[simp]
theorem toIcoDiv_add_zsmul' (a b : α) (m : ℤ) : toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m :=
  by
  refine toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_
  rw [sub_smul, ← sub_add, add_right_comm]
  simpa using sub_toIcoDiv_zsmul_mem_Ico hp a b

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