Nat.lcm_zero_left
theorem Nat.lcm_zero_left : ∀ (m : ℕ), Nat.lcm 0 m = 0
The theorem `Nat.lcm_zero_left` states that for any natural number `m`, the least common multiple of `0` and `m` is `0`. In mathematical terms, this would be represented as $\operatorname{lcm}(0, m) = 0$ for all natural numbers `m`. This is consistent with the general mathematical principle that the least common multiple of any number and zero is zero, as zero multiplied by any number always results in zero.
More concisely: The least common multiple of 0 and any natural number is 0.
|
Nat.lcm_ne_zero
theorem Nat.lcm_ne_zero : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0
This theorem states that for any two natural numbers `m` and `n`, if neither `m` nor `n` are zero, then their least common multiple (lcm) is also not zero. The least common multiple is defined as the product of `m` and `n` divided by their greatest common divisor (gcd).
More concisely: For any non-zero natural numbers m and n, their least common multiple is a non-zero number. (lcm(m, n) = (m * n) / gcd(m, n) where m and n are non-zero)
|
Nat.gcd_mul_lcm
theorem Nat.gcd_mul_lcm : ∀ (m n : ℕ), m.gcd n * m.lcm n = m * n
The theorem `Nat.gcd_mul_lcm` states that for any two natural numbers `m` and `n`, the product of the greatest common divisor (gcd) of `m` and `n` and the least common multiple (lcm) of `m` and `n` is equal to the product of `m` and `n`. In mathematical terms, for all natural numbers `m` and `n`, we have $\text{gcd}(m, n) \times \text{lcm}(m, n) = m \times n$.
More concisely: The greatest common divisor of natural numbers `m` and `n` multiplied by their least common multiple equals the product of `m` and `n`: $\text{gcd}(m, n) \times \text{lcm}(m, n) = m \times n$.
|
Nat.lcm_dvd
theorem Nat.lcm_dvd : ∀ {m n k : ℕ}, m ∣ k → n ∣ k → m.lcm n ∣ k
This theorem states that for any three natural numbers `m`, `n`, and `k`, if `m` divides `k` and `n` divides `k`, then the least common multiple of `m` and `n` also divides `k`. In mathematical notation, we have: if $m | k$ and $n | k$, then $\text{lcm}(m, n) | k$. The least common multiple (lcm) is defined as the product of `m` and `n` divided by their greatest common divisor (gcd).
More concisely: If `m` and `n` are natural numbers that divide `k`, then their least common multiple `lcm(m, n)` also divides `k`.
|
Nat.dvd_lcm_left
theorem Nat.dvd_lcm_left : ∀ (m n : ℕ), m ∣ m.lcm n
This theorem states that for all natural numbers `m` and `n`, `m` divides the least common multiple of `m` and `n`. In mathematical terms, for every pair of natural numbers $m, n$, $m$ is a divisor of their least common multiple (LCM).
More concisely: For all natural numbers m and n, m | LCM(m, n). (Here, "|" represents the divisibility relation.)
|
Nat.dvd_lcm_right
theorem Nat.dvd_lcm_right : ∀ (m n : ℕ), n ∣ m.lcm n
The theorem `Nat.dvd_lcm_right` states that for any two natural numbers `m` and `n`, `n` divides the least common multiple of `m` and `n`. In other words, `n` is a factor of the least common multiple of `m` and `n`. In mathematical terms, this can be written as: for all natural numbers `m` and `n`, `n` divides `LCM(m, n)`.
More concisely: For all natural numbers m and n, n divides the least common multiple of m and n.
|