toIocMod_zsmul_add' — Mathlib

English

Let α be an ordered additive group with p > 0 and hp the Archimedean-related hypothesis. For all a, b ∈ α and m ∈ Z, the value of toIocMod hp (m·p + a) b equals m·p plus toIocMod hp a b.

Русский

Пусть α — упорядоченная аддитивная группа, p > 0, и hp удовлетворяет соответствующему архимедовому условию. Для любых a, b ∈ α и m ∈ Z значение toIocMod hp (m·p + a) b равно m·p плюс toIocMod hp a b.

LaTeX

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

Lean4

@[simp]
theorem toIocMod_zsmul_add' (a b : α) (m : ℤ) : toIocMod hp (m • p + a) b = m • p + toIocMod hp a b := by
  rw [add_comm, toIocMod_add_zsmul', add_comm]

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