toIocMod_sub

Mathlib.Algebra.Order.ToIntervalMod

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

English

For all a,b,c ∈ α, the relation holds: toIcoMod hp a (b − c) = toIcoMod hp (a + c) b − c.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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