toIcoDiv_sub_eq_toIcoDiv_add' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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