toIcoMod_add_zsmul

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

For any hp, a, b, c, toIcoDiv hp (a − c) b = toIcoDiv hp a (b + c).

Русский

Для любого hp, a, b, c выполняется toIcoDiv hp (a − c) b = toIcoDiv hp a (b + c).

LaTeX

$$$\operatorname{toIcoDiv}\\_{hp}(a - c, b) = \operatorname{toIcoDiv}\\_{hp} a\\, (b + c)$$$

Lean4

@[simp]
theorem toIcoMod_add_zsmul (a b : α) (m : ℤ) : toIcoMod hp a (b + m • p) = toIcoMod hp a b :=
  by
  rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, add_smul]
  abel

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

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

Разделы

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

Аффилиация

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