toIcoMod_add_toIocMod_zero

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIcoMod_add_toIocMod_zero

English

The sum of the two complementary modulo interval values from a to b and from b to a equals p.

Русский

Сумма значений IcoMod и IocMod равна p.

LaTeX

$$$$ \operatorname{toIcoMod}(hp, 0, a-b) + \operatorname{toIocMod}(hp, 0, (b-a)) = p $$$$

Lean4

theorem toIcoMod_add_toIocMod_zero (a b : α) : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p := by
  rw [toIcoMod_zero_sub_comm, sub_add_cancel]

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

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

Разделы

Аффилиация

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