toIocMod_sub_zsmul — Mathlib

English

In a suitable Archimedean ordered additive group, for all a, b ∈ α and m ∈ Z, we have toIocMod hp a (b − m·p) = toIocMod hp a b.

Русский

В подходящей архимедовой упорядоченной аддитивной группе выполняется toIocMod hp a (b − m·p) = toIocMod hp a b.

LaTeX

$$$\forall a,b \in \alpha\,\forall m \in \mathbb{Z},\; toIocMod\ hp\ a\ (b - m\cdot p) = toIocMod\ hp\ a\ b$$$

Lean4

@[simp]
theorem toIocMod_sub_zsmul (a b : α) (m : ℤ) : toIocMod hp a (b - m • p) = toIocMod hp a b := by
  rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]

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