mul_den_eq_num — Mathlib

English

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

Русский

Для любого q ∈ ℚ произведение q на его знаменатель равно числителю.

LaTeX

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

Lean4

@[simp]
theorem mul_den_eq_num (q : ℚ) : q * q.den = q.num :=
  by
  suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by simp_all
  have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero
  rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

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