eq_num_of_isInt

Mathlib.Data.Rat.Defs

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

← MathLib Explorer

English

If a rational q is an integer, then q equals its numerator as a rational.

Русский

Если q является целым, то q = q.num как рациональное число.

LaTeX

$$$q.den = 1 \Rightarrow q = q.num$$$

Lean4

theorem eq_num_of_isInt {q : ℚ} (h : q.isInt) : q = q.num :=
  by
  rw [Rat.isInt, Nat.beq_eq_true_eq] at h
  exact (Rat.coe_int_num_of_den_eq_one h).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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