Int.coe_nat_dvd
theorem Int.coe_nat_dvd : ∀ {m n : ℕ}, ↑m ∣ ↑n ↔ m ∣ n
This theorem, named `Int.coe_nat_dvd`, is an alias of `Int.natCast_dvd_natCast`. It states that for all natural numbers `m` and `n`, `m` divides `n` if and only if the integer cast of `m` divides the integer cast of `n`. In other words, the divisibility relationship between `m` and `n` is preserved when they are cast to integers.
More concisely: For all natural numbers m and n, m | n if and only if (cast m to Int) | (cast n to Int), where "|" denotes divisibility.
|
Int.coe_nat_dvd_left
theorem Int.coe_nat_dvd_left : ∀ {n : ℕ} {z : ℤ}, ↑n ∣ z ↔ n ∣ z.natAbs
The theorem `Int.coe_nat_dvd_left` states that for any natural number `n` and any integer `z`, `n` divides `z` (in the sense of integers) if and only if `n` divides the absolute value of `z` (in the sense of natural numbers). Here, "divides" means that there exists another integer such that when `n` (or `z`) is multiplied by this integer, the result is `z` (or the absolute value of `z`), respectively. The absolute value of an integer is calculated as described in the `Int.natAbs` function: if the integer is non-negative, it is unchanged; if the integer is negative, its sign is changed to positive.
More concisely: For any integer `z` and natural number `n`, `n` divides `z` if and only if `n` divides the absolute value of `z`.
|