intCast_div_eq_divInt

Mathlib.Data.Rat.Defs

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

English

For integers n, d, the rational obtained by casting n to ℚ and dividing by d equals the divInt representation n /. d.

Русский

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

LaTeX

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

Lean4

theorem intCast_div_eq_divInt (n d : ℤ) : (n : ℚ) / d = n /. d := by rw [divInt_eq_div]

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

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

Разделы

Аффилиация

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