ceil_intCast_div_natCast

Mathlib.Data.Rat.Floor

URI: https://scilib.ai/kg/mathlib#Rat.ceil_intCast_div_natCast

← MathLib Explorer

English

For n,d ∈ ℕ, ⌈(n/d)⌉ = -((-n)/d).

Русский

Для n,d ∈ ℕ, ⌈n/d⌉ = -((-n)/d).

LaTeX

$$$\lceil \dfrac{n}{d} \rceil = -\left(-\dfrac{n}{d}\right)$$$

Lean4

@[norm_cast]
theorem ceil_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / (↑d : ℤ)) :=
  by
  conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]
  rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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