toIcoDiv_sub_zsmul' — Mathlib

English

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

Русский

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

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