floor_sub_intCast

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.floor_sub_intCast

English

For a ∈ R and z ∈ ℤ: ⌊a − z⌋ = ⌊a⌋ − z.

Русский

Для любого a ∈ R и z ∈ ℤ: ⌊a − z⌋ = ⌊a⌋ − z.

LaTeX

$$$$\forall a \in R,\ z \in \mathbb{Z}:\ \left\lfloor a - z \right\rfloor = \left\lfloor a \right\rfloor - z.$$$$

Lean4

@[simp]
theorem floor_sub_intCast (a : R) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
  Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (floor_add_intCast _ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru