toIocMod_add_right

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

In the same Archimedean setting, toIocMod hp a (b + p) = toIocMod hp a b.

Русский

В той же архимедовой конфигурации toIocMod hp a (b + p) = toIocMod hp a b.

LaTeX

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

Lean4

@[simp]
theorem toIocMod_add_right (a b : α) : toIocMod hp a (b + p) = toIocMod hp a b := by
  simpa only [one_zsmul] using toIocMod_add_zsmul hp a b 1

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

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

Разделы

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

Аффилиация

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