Rat.mul_den_eq_num
theorem Rat.mul_den_eq_num : ∀ {q : ℚ}, q * ↑q.den = ↑q.num
This theorem states that for any rational number `q`, the product of `q` and the denominator of `q` (when the denominator is promoted to a rational number) is equal to the numerator of `q` (when the numerator is promoted to a rational number). In mathematical terms, for any rational number (q = p/q), the equation `q * denom(q) = num(q)` holds.
More concisely: For any rational number q = p/q, the product of q and its denominator is equal to its numerator: q * denom(q) = num(q).
|
Rat.exists_eq_mul_div_num_and_eq_mul_div_den
theorem Rat.exists_eq_mul_div_num_and_eq_mul_div_den :
∀ (n : ℤ) {d : ℤ}, d ≠ 0 → ∃ c, n = c * (↑n / ↑d).num ∧ d = c * ↑(↑n / ↑d).den
This theorem states that for any integer `n` and any non-zero integer `d`, there exists an integer `c` such that `n` equals `c` times the numerator of the rational number `n/d`, and `d` equals `c` times the denominator of this rational number. In other words, it shows that `n` and `d` can be expressed as multiples of the respective parts of the fraction `n/d`.
More concisely: For any integer `n` and non-zero integer `d`, there exist integers `c` such that `n = c * (numerator (nat_num_div n d)` and `d = c * (denominator (nat_num_div n d))`.
|