Int.coe_natAbs
theorem Int.coe_natAbs : ∀ (n : ℤ), ↑n.natAbs = |n|
This theorem, referred to as an alias of `Int.natCast_natAbs`, states that for any integer `n`, the natural number obtained by applying the `Int.natAbs` function on `n` is equal to the absolute value of `n`. Here, `↑(Int.natAbs n)` represents the natural number cast as an integer. Essentially, it affirms that the absolute value operation on an integer and the `Int.natAbs` function (which returns the absolute value of an integer as a natural number) are equivalent when the natural number is cast back into an integer.
More concisely: For any integer `n`, `Int.natAbs n = abs n` holds, where `abs` denotes the absolute value and `Int.natAbs` returns the absolute value as a natural number and then is cast back to an integer.
|
Int.coe_nat_ne_zero_iff_pos
theorem Int.coe_nat_ne_zero_iff_pos : ∀ {n : ℕ}, ↑n ≠ 0 ↔ 0 < n
This theorem, `Int.coe_nat_ne_zero_iff_pos`, is essentially an alias of `Int.natCast_ne_zero_iff_pos`. It asserts a bi-conditional relationship between a natural number `n` not being 0 when cast to an integer and `n` being greater than 0. In other words, a natural number `n` is greater than 0 if and only if `n` is not equal to 0 when converted to an integer.
More concisely: A natural number `n` is greater than 0 if and only if the integer `n` is not equal to 0.
|
Int.coe_nat_eq_zero
theorem Int.coe_nat_eq_zero : ∀ {n : ℕ}, ↑n = 0 ↔ n = 0
This theorem, `Int.coe_nat_eq_zero`, is an alias of `Int.natCast_eq_zero`. It states that for any natural number `n`, the integer cast of `n` is equal to zero if and only if `n` is itself zero. In other words, a natural number `n` is zero if and only if its corresponding integer is also zero.
More concisely: For any natural number `n`, the integer cast of `n` equals zero if and only if `n` is zero. (In other words, `n = 0` if and only if `toInt n = 0`.)
|
Int.coe_nat_ne_zero
theorem Int.coe_nat_ne_zero : ∀ {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
This theorem, `Int.coe_nat_ne_zero`, is an alias of `Int.natCast_ne_zero`. It states that for all natural numbers `n`, the coerced value of `n` to an integer is not equal to zero if and only if `n` is not equal to zero. In other words, it provides a condition to check whether a natural number is not zero by checking whether its integer representation is not zero.
More concisely: For any natural number n, the coerced integer of n is not equal to zero if and only if n is not equal to zero.
|
Int.natAbs_inj_of_nonneg_of_nonneg
theorem Int.natAbs_inj_of_nonneg_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a.natAbs = b.natAbs ↔ a = b)
This theorem, `Int.natAbs_inj_of_nonneg_of_nonneg`, states that for any two non-negative integers `a` and `b` (i.e., `a` and `b` are greater than or equal to 0), the equality of the absolute values of `a` and `b` implies the equality of `a` and `b` itself. In other words, if `a` and `b` are non-negative integers and the absolute value of `a` is the same as the absolute value of `b`, then `a` must equal `b`.
More concisely: For non-negative integers `a` and `b`, if `|a| = |b|`, then `a = b`.
|