toIocMod_neg

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

For all a,b ∈ α, the identity toIocMod hp a (−b) = p − toIcoMod hp (−a) b holds.

Русский

Для любых a,b ∈ α выполняется: toIocMod hp a (−b) = p − toIcoMod hp (−a) b.

LaTeX

$$$\forall a,b \in \alpha,\; toIocMod\ hp\ a\ (-b) = p - toIcoMod\ hp\ (-a)\ b$$$

Lean4

theorem toIocMod_neg (a b : α) : toIocMod hp a (-b) = p - toIcoMod hp (-a) b :=
  by
  simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]
  abel

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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