coe_int_num_of_den_eq_one

Mathlib.Data.Rat.Defs

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

← MathLib Explorer

English

If a rational q has denominator 1, then it equals its numerator as a rational.

Русский

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

LaTeX

$$$q.den = 1 \Rightarrow (q.num : \mathbb{Q}) = q$$$

Lean4

theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q :=
  by
  conv_rhs => rw [← num_divInt_den q, hq]
  rw [intCast_eq_divInt]
  rfl

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

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

Разделы

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

Аффилиация

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