self_sub_toIocMod

Mathlib.Algebra.Order.ToIntervalMod

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

English

b − toIocMod hp a b equals toIocDiv hp a b times p.

Русский

b − toIocMod hp a b = toIocDiv hp a b · p.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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