natCast_div_eq_divInt

Mathlib.Data.Rat.Defs

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

English

For natural numbers n, d, the rational (n : ℚ) / d equals n /. d.

Русский

Для натуральных n, d верно, что (n : ℚ) / d = n /. d.

LaTeX

$$$(n : \mathbb{Q}) / d = n /. d$$$

Lean4

theorem natCast_div_eq_divInt (n d : ℕ) : (n : ℚ) / d = n /. d :=
  Rat.intCast_div_eq_divInt n d

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

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

Разделы

Аффилиация

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