toIcoMod_add_toIcoDiv_zsmul — Mathlib

English

Let α be an Archimedean ordered additive group and p > 0. For all a, b in α, b can be written as b = r + q p where r = toIcoMod(hp, a, b) and q = toIcoDiv(hp, a, b); moreover r ∈ [a, a + p) and q ∈ ℤ.

Русский

Пусть α — упорядоченная аддитивная группа с Архимедовым свойством, и p > 0. Для любых a, b ∈ α существует разложение b = r + q p, где r = toIcoMod(hp, a, b), q = toIcoDiv(hp, a, b); при этом r ∈ [a, a + p) и q ∈ ℤ.

LaTeX

$$$$\text{toIcoMod}(hp, a, b) + \text{toIcoDiv}(hp, a, b) \cdot p = b$$$$

Lean4

@[simp]
theorem toIcoMod_add_toIcoDiv_zsmul (a b : α) : toIcoMod hp a b + toIcoDiv hp a b • p = b := by
  rw [toIcoMod, sub_add_cancel]

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