toIcoDiv_add_right

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

For all a, b ∈ α, toIcoDiv(hp, a, b + p) = toIcoDiv(hp, a, b) + 1.

Русский

Для любых a, b ∈ α: toIcoDiv(hp, a, b + p) = toIcoDiv(hp, a, b) + 1.

LaTeX

$$$$\text{toIcoDiv}(hp, a, b + p) = \text{toIcoDiv}(hp, a, b) + 1$$$$

Lean4

@[simp]
theorem toIcoDiv_add_right (a b : α) : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1 := by
  simpa only [one_zsmul] using toIcoDiv_add_zsmul hp a b 1

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

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

Разделы

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

Аффилиация

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