self_sub_toIocDiv_zsmul

Mathlib.Algebra.Order.ToIntervalMod

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

English

The relation toIocDiv hp a b • p − b equals the negation of toIocMod hp a b.

Русский

Соотношение: toIocDiv hp a b • p − b = −toIocMod hp a b.

LaTeX

$$$ \mathrm{toIocDiv}(hp,a,b)\cdot p - b = -\mathrm{toIocMod}(hp,a,b) $$$

Lean4

@[simp]
theorem self_sub_toIocDiv_zsmul (a b : α) : b - toIocDiv hp a b • p = toIocMod hp a b :=
  rfl

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

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

Разделы

Аффилиация

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