toIocMod_sub'

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIocMod_sub'

← MathLib Explorer

English

For all a,b ∈ α, we have toIcoMod hp (a − p) b = toIcoMod hp a b − p.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toIocMod_sub' (a b : α) : toIocMod hp (a - p) b = toIocMod hp a b - p := by
  simpa only [one_zsmul] using toIocMod_sub_zsmul' hp a b 1

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

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

Разделы

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

Аффилиация

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