toIcoMod_sub_zsmul — Mathlib

English

In an Archimedean ordered additive group, for all a, b ∈ α and m ∈ Z, the value of toIcoMod hp a (b − m·p) is equal to toIcoMod hp a b.

Русский

В упорядоченной архимедовой аддитивной группе для любых a, b ∈ α и m ∈ Z значение toIcoMod hp a (b − m·p) равно toIcoMod hp a b.

LaTeX

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

Lean4

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

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