toIocDiv_neg'

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIocDiv_neg'

English

A variant of negation: toIcoDiv hp (−a) b = −(toIocDiv hp a (−b) + 1).

Русский

Вариант негирования: toIcoDiv hp (−a) b = −(toIocDiv hp a (−b) + 1).

LaTeX

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

Lean4

theorem toIocDiv_neg' (a b : α) : toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1) := by
  simpa only [neg_neg] using toIocDiv_neg hp (-a) (-b)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru