exists_eq_mul_div_num_and_eq_mul_div_den

English

There exists an integer c such that n = c * ((n : ℚ) / d).num and d = c * ((n : ℚ) / d).den, provided d ≠ 0.

Русский

Существует целое c такое, что n = c · ((n : ℚ) / d).num и d = c · ((n : ℚ) / d).den при условии d ≠ 0.

LaTeX

$$$\exists c : \mathbb{Z}, n = c \cdot ((n : \mathbb{Q}) / d).num \land (d : \mathbb{Z}) = c \cdot ((n : \mathbb{Q}) / d).den$$$

Lean4

theorem exists_eq_mul_div_num_and_eq_mul_div_den (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :
    ∃ c : ℤ, n = c * ((n : ℚ) / d).num ∧ (d : ℤ) = c * ((n : ℚ) / d).den :=
  haveI : (n : ℚ) / d = Rat.divInt n d := by rw [← Rat.divInt_eq_div]
  Rat.num_den_mk d_ne_zero this

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