floor_natCast_div_natCast

Mathlib.Data.NNRat.Floor

URI: https://scilib.ai/kg/mathlib#NNRat.floor_natCast_div_natCast

English

For natural numbers n, d, the floor of (↑n / ↑d) in ℚ≥0 equals n ÷ d (integer division).

Русский

Для натуральных n, d полуfloor (↑n / ↑d) в ℚ≥0 равен n ÷ d (целочисленное деление).

LaTeX

$$⌊(↑n / ↑d : ℚ≥0)⌋_{+} = n ÷ d$$

Lean4

@[norm_cast]
theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊ = n / d :=
  Rat.natFloor_natCast_div_natCast n d

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

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

Разделы

Аффилиация

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