toIocDiv_add_zsmul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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