toIcoDiv_zsmul_sub_self

Mathlib.Algebra.Order.ToIntervalMod

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

English

The relation toIcoDiv hp a b • p − b equals the negation of toIcoMod hp a b.

Русский

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

LaTeX

$$$ \mathrm{toIcoDiv}(hp,a,b)\cdot p - b = -\mathrm{toIcoMod}(hp,a,b) $$$

Lean4

@[simp]
theorem toIcoDiv_zsmul_sub_self (a b : α) : toIcoDiv hp a b • p - b = -toIcoMod hp a b := by rw [toIcoMod, neg_sub]

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

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

Разделы

Аффилиация

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