round_sub_intCast — Mathlib

English

In a linearly ordered ring with a floor operation, rounding commutes with subtraction by an integer: for every x and every integer y, round(x − y) = round(x) − y.

Русский

В упорядоченном кольце с операцией floor округление commuting по вычитанию целого: для всякого x и целого y выполняется round(x − y) = round(x) − y.

LaTeX

$$$\\\\forall x \in \alpha, \\\\\\forall y \in \mathbb{Z}, \\\\\\operatorname{round}(x - y) = \\\\\\operatorname{round}(x) - y.$$$

Lean4

@[simp]
theorem round_sub_intCast (x : α) (y : ℤ) : round (x - y) = round x - y :=
  by
  rw [sub_eq_add_neg]
  norm_cast
  rw [round_add_intCast, sub_eq_add_neg]

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