toIcoDiv_sub_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_sub_zsmul (a b : α) (m : ℤ) : toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m := by
  rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]

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