toIocDiv_zsmul_sub_self

Mathlib.Algebra.Order.ToIntervalMod

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

English

The equality toIocDiv hp a b • p − b equals −toIocMod hp a b.

Русский

Неравенство: toIocDiv hp a b • p − b = −toIocMod hp a b.

LaTeX

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

Lean4

@[simp]
theorem toIocDiv_zsmul_sub_self (a b : α) : toIocDiv hp a b • p - b = -toIocMod hp a b := by rw [toIocMod, neg_sub]

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

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

Разделы

Аффилиация

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