toIocDiv_neg — Mathlib

English

Negating the second argument relates to a combination of IocDiv and a shift: toIcoDiv hp a (−b) = −(toIocDiv hp (−a) b + 1).

Русский

Нега второго аргумента относится к сочетанию IocDiv и сдвига: toIcoDiv hp a (−b) = −(toIocDiv hp (−a) b + 1).

LaTeX

$$$\operatorname{toIcoDiv}\\_{hp} a ( - b ) = -(\operatorname{toIocDiv}\\_{hp}(-a) b + 1)$$$

Lean4

theorem toIocDiv_neg (a b : α) : toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1) := by
  rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_right]

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