toIocMod_add_toIocDiv_zsmul — Mathlib

English

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

Русский

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

LaTeX

$$$$\text{toIocMod}(hp, a, b) + \text{toIocDiv}(hp, a, b) \cdot p = b$$$$

Lean4

@[simp]
theorem toIocMod_add_toIocDiv_zsmul (a b : α) : toIocMod hp a b + toIocDiv hp a b • p = b := by
  rw [toIocMod, sub_add_cancel]

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