mul_den_eq_num

Mathlib.Data.NNRat.Defs

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

← MathLib Explorer

English

For any q ∈ ℚ≥0, q.den · q = q.num.

Русский

Для любого q ∈ ℚ≥0, q.den · q = q.num.

LaTeX

$$$ q.den \cdot q = q.num $$$

Lean4

@[simp]
theorem mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num := by
  ext
  push_cast
  rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]
  exact Rat.mul_den_eq_num _

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

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

Разделы

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

Аффилиация

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