Int.ofNat_eq_coe
theorem Int.ofNat_eq_coe : ∀ {n : ℕ}, Int.ofNat n = ↑n
This theorem states that for every natural number `n`, the function `Int.ofNat n` (which converts a natural number to an integer) is equal to the coercion of `n` to an integer, denoted by `↑n`. In other words, it expresses that these two ways of turning a natural number into an integer are identical.
More concisely: For every natural number `n`, `Int.ofNat n` equals the coercion `↑n`.
|
Int.ofNat_zero
theorem Int.ofNat_zero : ↑0 = 0
This theorem, `Int.ofNat_zero`, states that the integer value of the natural number 0 is also 0. In other words, when a natural number 0 is converted to an integer in Lean 4, it remains 0.
More concisely: The theorem asserts that the natural number 0 converts to the integer 0 in Lean 4.
|
Int.ofNat_one
theorem Int.ofNat_one : ↑1 = 1
This is a theorem named `Int.ofNat_one` in Lean 4, which states that the integer representation of the natural number 1 is equal to 1. In other words, when the natural number 1 is cast to an integer, the resulting integer is still 1.
More concisely: The theorem `Int.ofNat_one` in Lean 4 asserts that the conversion of the natural number 1 to an integer results in the integer 1. In mathematical notation, 1 = (1 : int).
|
Int.ofNat.inj
theorem Int.ofNat.inj : ∀ {a a_1 : ℕ}, Int.ofNat a = Int.ofNat a_1 → a = a_1
The theorem `Int.ofNat.inj` states that for any two natural numbers `a` and `a_1`, if their corresponding integer representations obtained by the function `Int.ofNat` are equal, then `a` and `a_1` are also equal. In other words, `Int.ofNat` is an injective function from the set of natural numbers to the set of integers.
More concisely: The function `Int.ofNat` maps distinct natural numbers to distinct integers.
|