toIocDiv_zsmul_add

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

For all a, b ∈ α and m ∈ ℤ, toIocDiv(hp, a, m p + b) = m + toIocDiv(hp, a, b).

Русский

Для любых a, b ∈ α и m ∈ ℤ: toIocDiv(hp, a, m p + b) = m + toIocDiv(hp, a, b).

LaTeX

$$$$\text{toIocDiv}(hp, a, m p + b) = m + \text{toIocDiv}(hp, a, b)$$$$

Lean4

@[simp]
theorem toIocDiv_zsmul_add (a b : α) (m : ℤ) : toIocDiv hp a (m • p + b) = m + toIocDiv hp a b := by
  rw [add_comm, toIocDiv_add_zsmul, add_comm]

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

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

Разделы

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

Аффилиация

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