toIcoMod_sub_self

Mathlib.Algebra.Order.ToIntervalMod

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

English

toIcoMod hp a b − b equals the negation of toIcoDiv hp a b times p.

Русский

toIcoMod hp a b − b = − toIcoDiv hp a b · p.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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