ceil_natCast_div_natCast

Mathlib.Data.Rat.Floor

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

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_natCast_div_natCast (n d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / d) :=
  ceil_intCast_div_natCast n d

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

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

Разделы

Аффилиация

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