toIcoDiv_add_right' — Mathlib

English

Let α be an Archimedean ordered additive group with a positive p. For any a, b ∈ α, the shifted right increment satisfies toIcoDiv hp (a + p) b = toIcoDiv hp a b − 1.

Русский

Пусть α — упорядоченная аддитивная группа с архимедовым свойством и p > 0. Для любых a, b ∈ α выполняется: toIcoDiv hp (a + p) b = toIcoDiv hp a b − 1.

LaTeX

$$$\operatorname{toIcoDiv}\\_{hp}(a + p, b) = \operatorname{toIcoDiv}\\_{hp}(a, b) - 1$$$

Lean4

@[simp]
theorem toIcoDiv_add_right' (a b : α) : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1 := by
  simpa only [one_zsmul] using toIcoDiv_add_zsmul' hp a b 1

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