toIcoMod_add_right — Mathlib

English

In an Archimedean ordered additive group, adding p to the second argument does not change the IcoMod value: toIcoMod hp a (b + p) = toIcoMod hp a b.

Русский

В архимедовой упорядоченной аддитивной группе прибавление p ко второму аргументу не изменяет значение IcoMod: toIcoMod hp a (b + p) = toIcoMod hp a b.

LaTeX

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

Lean4

@[simp]
theorem toIcoMod_add_right (a b : α) : toIcoMod hp a (b + p) = toIcoMod hp a b := by
  simpa only [one_zsmul] using toIcoMod_add_zsmul hp a b 1

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