ceilDiv_eq_add_pred_div

Mathlib.Algebra.Order.Floor.Div

URI: https://scilib.ai/kg/mathlib#Nat.ceilDiv_eq_add_pred_div

English

For all natural numbers a and b, ceilDiv a b equals (a + b − 1) / b.

Русский

Для любых a, b ∈ ℕ верно: ceilDiv a b = (a + b − 1) / b.

LaTeX

$$$$ a \\lceil/\\rceil b = \\frac{a + b - 1}{b} $$$$

Lean4

theorem ceilDiv_eq_add_pred_div (a b : ℕ) : a ⌈/⌉ b = (a + b - 1) / b :=
  rfl

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

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

Разделы

Аффилиация

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