toIcoMod_neg

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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