Rat.divInt_ne_zero
theorem Rat.divInt_ne_zero : ∀ {a b : ℤ}, b ≠ 0 → (Rat.divInt a b ≠ 0 ↔ a ≠ 0)
The theorem `Rat.divInt_ne_zero` states that for all integers `a` and `b`, if `b` is not equal to zero, then the quotient of `a` divided by `b` (using the function `Rat.divInt`) is not equal to zero if and only if `a` is not equal to zero. In other words, a nonzero integer divided by another nonzero integer will give a nonzero rational number, and vice versa.
More concisely: For all integers a and b, Rat.divInt a b ≠ 0 if and only if a ≠ 0 and b ≠ 0.
|
Rat.num_div_den
theorem Rat.num_div_den : ∀ (r : ℚ), ↑r.num / ↑r.den = r
This theorem states that for all rational numbers 'r', when the numerator of 'r' is divided by the denominator of 'r', it equals 'r'. Here, `ℚ` represents the set of all rational numbers, `r.num` represents the numerator of 'r', and `r.den` represents the denominator of 'r'. The ↑ operator is used for type casting, converting the integers `r.num` and `r.den` to rational numbers.
More concisely: For all rational numbers r, r = r.num / r.den.
|
Rat.zero_of_num_zero
theorem Rat.zero_of_num_zero : ∀ {q : ℚ}, q.num = 0 → q = 0
This theorem states that for any rational number `q`, if the numerator of `q` is zero, then `q` itself must be zero. In mathematical terms, if we have a rational number represented as `q = p/q`, and if `p = 0`, then `q` must also be 0, regardless of the value of `q`.
More concisely: If the numerator of a rational number is zero, then the rational number is equal to zero.
|
Rat.divInt_eq_div
theorem Rat.divInt_eq_div : ∀ (n d : ℤ), Rat.divInt n d = ↑n / ↑d
This theorem states that for any two integers `n` and `d`, the function `Rat.divInt` applied to `n` and `d` is equal to the division of the rational numbers corresponding to `n` and `d` respectively. In other words, for any integers `n` and `d`, the operation of forming the rational number quotient using `Rat.divInt` is equivalent to first converting those integers to rational numbers (indicated by the ↑ notation) and then performing the division operation.
More concisely: For any integers `n` and `d`, `Rat.divInt n d = Rat.castFromInt n / Rat.castFromInt d`.
|
Rat.eq_iff_mul_eq_mul
theorem Rat.eq_iff_mul_eq_mul : ∀ {p q : ℚ}, p = q ↔ p.num * ↑q.den = q.num * ↑p.den
This theorem states that for any two rational numbers `p` and `q`, `p` is equal to `q` if and only if the numerator of `p` multiplied by the denominator of `q` is equal to the numerator of `q` multiplied by the denominator of `p`. In mathematical terms, we have p = q if and only if p.num * q.den = q.num * p.den. This is essentially a restatement of the cross-multiplication rule in the context of rational numbers.
More concisely: For rational numbers p and q, p = q if and only if p.num * q.den = q.num * p.den (cross-multiplication rule).
|
Rat.inv_def'
theorem Rat.inv_def' : ∀ (q : ℚ), q⁻¹ = Rat.divInt (↑q.den) q.num
This theorem states that for any two integers `a` and `b`, the reciprocal of the rational number formed by dividing `a` by `b` is the same as the rational number formed by dividing `b` by `a`. In other words, it expresses the property $(\frac{a}{b})^{-1} = \frac{b}{a}$ for all integers `a` and `b`.
More concisely: The reciprocal of the rational number `a / b` is equal to `b / a` for all integers `a` and `b`.
|
Rat.coe_int_num_of_den_eq_one
theorem Rat.coe_int_num_of_den_eq_one : ∀ {q : ℚ}, q.den = 1 → ↑q.num = q
This theorem states that for any rational number `q`, if the denominator of `q` is equal to `1`, then the numerator of `q` as an integer is equal to `q` itself. In other words, it ensures that when the denominator of a rational number is `1`, the rational number is essentially an integer.
More concisely: For any rational number `q` with denominator `1`, its numerator is equal to `q`.
|
Rat.neg_def
theorem Rat.neg_def : ∀ (q : ℚ), -q = Rat.divInt (-q.num) ↑q.den
The theorem `Rat.neg_def` states that for any two integers `a` and `b`, the negation of the quotient of `a` by `b` is equal to the quotient of the negation of `a` and `b`. In other words, it asserts that the operation of negation commutes with the division operation for integers (casted to rational numbers), i.e., we have `- (a / b) = (-a) / b` for all integers `a` and `b`.
More concisely: For all integers a and b, $-(a / b) = (-a) / b$.
|
Rat.pos
theorem Rat.pos : ∀ (a : ℚ), 0 < a.den
This theorem states that for every rational number `a`, the denominator of `a` is greater than zero. In other words, the denominator of any rational number must always be a positive integer.
More concisely: Every rational number has a positive denominator.
|
Rat.coe_int_eq_divInt
theorem Rat.coe_int_eq_divInt : ∀ (z : ℤ), ↑z = Rat.divInt z 1
This theorem states that for every integer `z`, the rational number equivalent of `z`, denoted as `↑z`, is equal to the result of dividing `z` by `1` using the `Rat.divInt` function. In other words, it demonstrates that the process of casting an integer to a rational number is equivalent to dividing that integer by 1 in the realm of rational numbers.
More concisely: For every integer `z`, `↑z = Rat.divInt z 1`.
|
Rat.add_def''
theorem Rat.add_def'' :
∀ {a b c d : ℤ}, b ≠ 0 → d ≠ 0 → Rat.divInt a b + Rat.divInt c d = Rat.divInt (a * d + c * b) (b * d)
The theorem `Rat.add_def''` states that for any four integers `a`, `b`, `c`, and `d`, where both `b` and `d` are non-zero, the sum of the rational numbers `a / b` and `c / d` (which are represented as `Rat.divInt a b` and `Rat.divInt c d` in Lean 4) is equal to the rational number `(a * d + c * b) / (b * d)`. In other words, the theorem is a formalization of the standard rule for adding fractions, where the numerator is the sum of the cross-products, and the denominator is the product of the denominators.
More concisely: For integers a, b, c, and d with b and d non-zero, (a/b + c/d) = ((a*d + b*c) / (b*d)).
|