floorDiv_eq_div

Mathlib.Algebra.Order.Floor.Div

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

English

For all natural numbers a and b, floor division by b coincides with ordinary division: a ⌊/⌋ b = a / b.

Русский

Для любых натуральных чисел a и b целочисленное деление a ⌊/⌋ b совпадает с обычным делением: a ⌊/⌋ b = a / b.

LaTeX

$$$$ a \\lfloor/\\rfloor b = a / b $$$$

Lean4

@[simp]
theorem floorDiv_eq_div (a b : ℕ) : a ⌊/⌋ b = a / b :=
  rfl

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

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

Разделы

Аффилиация

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