toIocDiv_sub_eq_toIocDiv_add' — Mathlib

English

For any a, b, c, the shifted sub-lemma holds: toIocDiv hp (a - c) b = toIocDiv hp a (b + c).

Русский

Для любых a, b, c выполняется: toIocDiv hp (a - c) b = toIocDiv hp a (b + c).

LaTeX

$$$\operatorname{toIocDiv}\\_{hp}(a - c, b) = \operatorname{toIocDiv}\\_{hp}\, a\\, (b + c)$$$

Lean4

theorem toIocDiv_sub_eq_toIocDiv_add' (a b c : α) : toIocDiv hp (a - c) b = toIocDiv hp a (b + c) := by
  rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg]

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