num_div_den

Mathlib.Algebra.Field.Rat

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

← MathLib Explorer

English

For q ∈ ℚ≥0, (q.num : ℚ≥0) / q.den = q.

Русский

Для q ∈ ℚ≥0 выполняется (q.num : ℚ≥0) / q.den = q.

LaTeX

$$$ (q.\num : \mathbb{Q}_{\ge 0}) / q.\den = q $$$

Lean4

@[simp]
theorem num_div_den (q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q :=
  by
  ext1
  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]
  exact (cast_def _).symm

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

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

Разделы

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

Аффилиация

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