toIocDiv_sub_zsmul' — Mathlib

English

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

Русский

Для любых 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_sub_zsmul' (a b : α) (m : ℤ) : toIocDiv hp (a - m • p) b = toIocDiv hp a b + m := by
  rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_eq_add]

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