num_div_den

Mathlib.Algebra.Ring.Rat

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

English

Let r ∈ ℚ with r.num = n and r.den = d. Then r = n/d in ℚ.

Русский

Пусть r ∈ ℚ имеет числитель n и знаменатель d. Тогда r = n/d в ℚ.

LaTeX

$$$\dfrac{r.num}{r.den} = r$$$

Lean4

theorem num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by
  rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]

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

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

Разделы

Аффилиация

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