Rat.num_nonneg
theorem Rat.num_nonneg : ∀ {a : ℚ}, 0 ≤ a.num ↔ 0 ≤ a
This theorem states that for any rational number 'a', the numerator of 'a' (a.num) is non-negative (greater than or equal to zero) if and only if 'a' itself is non-negative. In other words, it establishes that the sign of a rational number is determined by the sign of its numerator.
More concisely: For any rational number 'a', the numerator of 'a' is non-negative if and only if 'a' itself is non-negative. (Equivalently, the rational number 'a' has a non-negative numerator if and only if 'a' is non-negative.)
|
Rat.le_def
theorem Rat.le_def : ∀ {p q : ℚ}, p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
This theorem states that for any four integers `a`, `b`, `c`, and `d`, with both `b` and `d` being positive, the quotient of `a` and `b` (represented as `Rat.divInt a b`) is less than or equal to the quotient of `c` and `d` (represented as `Rat.divInt c d`) if and only if the product of `a` and `d` is less than or equal to the product of `c` and `b`. In mathematical terms, it is saying that $\frac{a}{b} \leq \frac{c}{d}$ if and only if $ad \leq cb$, under the condition that $b > 0$ and $d > 0$.
More concisely: For integers `a`, `b`, `c`, and `d` with `b` and `d` positive, `Rat.divInt a b <= Rat.divInt c d` if and only if `a * d <= c * b`.
|
Rat.divInt_nonneg
theorem Rat.divInt_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ Rat.divInt a b
This theorem, `Rat.divInt_nonneg`, states that for all integers `a` and for any integer `b` that is greater than zero, the quotient formed by dividing `a` by `b` is nonnegative if and only if `a` is nonnegative. In other words, a rational number obtained by dividing an integer `a` by a positive integer `b` is nonnegative exactly when `a` is nonnegative.
More concisely: For integers `a` and positive integer `b`, `a / b` is nonnegative if and only if `a` is nonnegative.
|