self_sub_toIcoMod

Mathlib.Algebra.Order.ToIntervalMod

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

English

b − toIcoMod hp a b equals toIcoDiv hp a b times p.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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