Int.gcd_dvd_left
theorem Int.gcd_dvd_left : ∀ {a b : ℤ}, ↑(a.gcd b) ∣ a
The theorem `Int.gcd_dvd_left` states that for any two integers `a` and `b`, the greatest common divisor (gcd) of `a` and `b` divides `a`. This is written in the Lean theorem prover as `↑(Int.gcd a b) ∣ a`, where `Int.gcd a b` computes the gcd of `a` and `b`, the `↑` operator converts that gcd from a natural number to an integer, and `∣` represents the "divides" relation. In mathematical terms, if $gcd(a, b) = d$, then $d | a$.
More concisely: The greatest common divisor of integers `a` and `b` divides `a`. In mathematical notation, if $gcd(a, b) = d$, then $d | a$.
|
Int.gcd_dvd_right
theorem Int.gcd_dvd_right : ∀ {a b : ℤ}, ↑(a.gcd b) ∣ b
This theorem states that for any two integers `a` and `b`, the greatest common divisor (GCD) of `a` and `b` (calculated as a nonnegative integer) is a divisor of `b`. In other words, `b` is a multiple of the GCD of `a` and `b`. Here, `∣` is the "divides" relation in integer arithmetic, so `↑(Int.gcd a b) ∣ b` means that `b` divided by the GCD of `a` and `b` yields an integer.
More concisely: For any integers `a` and `b`, the greatest common divisor `d` of `a` and `b` satisfies `d ∣ b`.
|