floor_natCast_div_natCast

Mathlib.Data.Rat.Floor

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

English

For n,d ∈ ℕ, the floor of (n/d) equals the integer division n/d.

Русский

Для n,d ∈ ℕ, ⌊(n/d)⌋ = n div d.

LaTeX

$$$\lfloor \dfrac{n}{d} \rfloor = \dfrac{n}{d}$$$

Lean4

@[norm_cast]
theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d :=
  floor_intCast_div_natCast n d

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

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

Разделы

Аффилиация

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