PosNum.cast_to_nat
theorem PosNum.cast_to_nat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : PosNum), ↑↑n = ↑n
This theorem, `PosNum.cast_to_nat`, states that for all types `α` which belong to the `AddMonoidWithOne` class, casting a positive number `n` to `α` via two successive upcasts (first to natural numbers, then to `α`) is the same as casting `n` directly to `α`. Here, `PosNum` refers to a positive number and `↑↑n` and `↑n` denote the double and single casting processes respectively.
More concisely: For all types `α` in the `AddMonoidWithOne` class, the double upcast of a positive number `n` from natural numbers to `α` is equal to the single upcast of `n` directly to `α`. In mathematical notation, `↑↑n = ↑n : ℕ → α`.
|
PosNum.lt_to_nat
theorem PosNum.lt_to_nat : ∀ {m n : PosNum}, ↑m < ↑n ↔ m < n
This theorem states that for all positive numbers `m` and `n`, the natural number representation of `m` is less than the natural number representation of `n` if and only if `m` is less than `n`. In other words, the relative ordering of two positive numbers remains the same whether we consider them as positive numbers or as their natural number counterparts.
More concisely: For all positive integers m and n, m < n if and only if m.to Nat < n.to Nat in Lean's type Nat, where to Nat is a conversion from the type of positive numbers to the type of natural numbers.
|
PosNum.to_nat_pos
theorem PosNum.to_nat_pos : ∀ (n : PosNum), 0 < ↑n
This theorem states that for any positive number `n` (type `PosNum`), when converted to a natural number (using the ↑ symbol), it will be greater than 0. In other words, any positive number remains strictly positive even when viewed as a natural number.
More concisely: For any positive number `n`, its natural number representation `↑n` is a positive natural number.
|
Num.toZNum_succ
theorem Num.toZNum_succ : ∀ (n : Num), n.succ.toZNum = n.toZNum.succ
This theorem, `Num.toZNum_succ`, states that for any natural number `n`, the function `Num.toZNum` applied to the successor of `n` (i.e., `n` plus one) is equal to the function `ZNum.succ` applied to `Num.toZNum n`. Essentially, this means that the operations of taking the successor of a number and converting a natural number to an integer number commute, or can be performed in any order to achieve the same result.
More concisely: For all natural numbers n, Num.toZNum (n + 1) = ZNum.succ (Num.toZNum n).
|
ZNum.le_to_int
theorem ZNum.le_to_int : ∀ {m n : ZNum}, ↑m ≤ ↑n ↔ m ≤ n
This theorem states that for any two arbitrary `ZNum` values `m` and `n`, the integer representation of `m` is less than or equal to the integer representation of `n` if and only if `m` is less than or equal to `n`. In other words, the relationship of less than or equal to between `m` and `n` is preserved when they are converted to integers.
More concisely: For any `ZNum` values `m` and `n`, `int.to_nat m <= int.to_nat n` if and only if `m <= n`.
|
ZNum.cast_add
theorem ZNum.cast_add : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (m n : ZNum), ↑(m + n) = ↑m + ↑n
This theorem states that for any type `α` that is an `AddGroupWithOne` (that is, a group with addition as operation and one as the identity element), the casting of the sum of any two ZNums `m` and `n` to the type `α` equals the sum of the casts of `m` and `n` to `α`. In other words, addition in ZNums commutes with casting to any additive group with one.
More concisely: For any `AddGroupWithOne` type `α`, the operation of casting the sum of two ZNumbers to `α` is commutative with the addition of their casts to `α`.
|
Num.ofNat'_succ
theorem Num.ofNat'_succ : ∀ {n : ℕ}, Num.ofNat' (n + 1) = Num.ofNat' n + 1
The theorem `Num.ofNat'_succ` states that for any natural number `n`, the function `Num.ofNat'` applied to the successor of `n` (i.e., `n + 1`) is equal to the function `Num.ofNat'` applied to `n` incremented by one. Essentially, the theorem is stating the property that the function `Num.ofNat'` preserves the successor operation on natural numbers.
More concisely: For all natural numbers `n`, `Num.ofNat' (succ n) = Num.ofNat' n + 1`.
|
Num.ofNat'_bit
theorem Num.ofNat'_bit :
∀ (b : Bool) (n : ℕ), Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
The theorem `Num.ofNat'_bit` states that for all boolean values `b` and all natural numbers `n`, the process of converting the natural number obtained by appending the digit `b` to the binary representation of `n` into a `Num` type, is the same as first converting `n` into a `Num` type and then appending the digit `b` to it. If `b` is true, the digit appended is `1`, and if `b` is false, the digit appended is `0`.
More concisely: For all natural numbers `n` and booleans `b`, converting `n` to `Num` with appended binary digit `b` is equal to first converting `n` to `Num` and then appending digit `b * 2^(size Nat.binNum n)`.
|
PosNum.cast_bit0
theorem PosNum.cast_bit0 : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α] (n : PosNum), ↑n.bit0 = bit0 ↑n
This theorem, `PosNum.cast_bit0`, states that for any type `α` which has a defined addition and a defined "one" element, and for any positive number `n`, the result of converting the `bit0` (which duplicates the number) of `n` from `PosNum` (the type for positive numbers in Lean) to `α` is equal to the `bit0` of the converted `n`. In other words, the process of duplicating a number (using `bit0`) and then converting it to another type is the same as first converting the number to the other type and then duplicating it.
More concisely: For any type `α` with addition and a one element, and for any positive number `n` in Lean's `PosNum`, the conversion of `n.bit0` to `α` is equal to the conversion of `n` to `α` followed by taking the `bit0`.
|
PosNum.of_to_nat
theorem PosNum.of_to_nat : ∀ (n : PosNum), ↑↑n = Num.pos n
This theorem states that for every positive number `n`, the double-coercion of `n` (which converts it first into a natural number and then into a number) gives the positive version of `n`. In other words, converting a positive number to a natural number and then to a generic number preserves its positivity. This can be symbolically represented in LaTeX as, for all positive numbers $n$, we have $n = \text{Num.pos} \ n$.
More concisely: For every positive number `n` in Lean, the double-coercion `n` to natural number and then to number equals the positive version of `n`. In mathematical notation, for all positive numbers $n$, we have $\text{Num.pos}\ n = n$.
|
PosNum.to_nat_to_int
theorem PosNum.to_nat_to_int : ∀ (n : PosNum), ↑↑n = ↑n
This theorem states that for any positive number `n` of type `PosNum`, the double coercion of `n` to natural number and then to integer is equal to the direct coercion of `n` to integer. Essentially, it ensures that converting a positive number to a natural number and then to an integer yields the same result as directly converting the positive number to an integer.
More concisely: For any positive number `n`, the double coercion from `PosNum` to `Nat` and then to `Int` equals the direct coercion from `PosNum` to `Int`. In mathematical notation: `(coe : PosNum → Nat) (coe : Nat → Int) (n : PosNum) = coe : PosNum → Int`.
|
Num.le_to_nat
theorem Num.le_to_nat : ∀ {m n : Num}, ↑m ≤ ↑n ↔ m ≤ n
This theorem, `Num.le_to_nat`, states that for any two numerical values `m` and `n`, the condition that the natural number cast of `m` is less than or equal to the natural number cast of `n` is equivalent to the condition that `m` is less than or equal to `n`. In other words, the order relation (less than or equal to) is preserved when we cast from the `Num` type to the `Nat` type in Lean 4.
More concisely: For any numerical values `m` and `n` in Lean 4, `m ≤ n` if and only if `natNum m ≤ natNum n`, where `natNum` denotes the function that casts a numerical value to a natural number.
|
Num.to_nat_inj
theorem Num.to_nat_inj : ∀ {m n : Num}, ↑m = ↑n ↔ m = n
This theorem states that for any two numbers `m` and `n` of the numeric type `Num`, the condition of their conversions to natural numbers being equal is equivalent to `m` and `n` being equal themselves. In other words, if the natural number representation of `m` equals the natural number representation of `n`, then `m` equals `n` and vice versa. The function `↑` is used here to convert a number from type `Num` to type `Nat` (natural numbers in Lean 4).
More concisely: For any numbers `m` and `n` of type `Num`, `↑m = ↑n` if and only if `m = n`.
|
Num.bit0_of_bit0
theorem Num.bit0_of_bit0 : ∀ (n : Num), bit0 n = n.bit0
The theorem `Num.bit0_of_bit0` states that for all numbers `n` of the type `Num`, the `bit0` function (which doubles a number `n`) produces the same result as the `Num.bit0` function (which appends a `0` to the end of `n`, effectively doubling it). Essentially, this theorem establishes the equivalence of two methods of doubling a number: one using addition and the other using bitwise operations.
More concisely: The theorem `Num.bit0_of_bit0` asserts that for all numbers `n` in Lean's `Num` type, `2 * n = 2 * (n % 2) + n`, where `%` denotes modulo arithmetic and `Num.bit0` is defined as `x % 2`.
|
ZNum.lt_to_int
theorem ZNum.lt_to_int : ∀ {m n : ZNum}, ↑m < ↑n ↔ m < n
This theorem establishes an equivalence between the less-than relation for two arbitrary `ZNum` numbers, `m` and `n`, and the less-than relation for their corresponding integer counterparts (obtained by casting `m` and `n` to integers). In other words, `m` is less than `n` if and only if the integer representation of `m` is less than the integer representation of `n`.
More concisely: For all `m` and `n` as `ZNum`, `m < n` if and only if to_int m < to_int n`.
Here, `to_int` is the function that converts a `ZNum` to an integer.
|
Num.mul_to_nat
theorem Num.mul_to_nat : ∀ (m n : Num), ↑(m * n) = ↑m * ↑n
This theorem states that for all numbers `m` and `n` of type `Num`, the casting of the product of `m` and `n` into a `Nat` (natural number) is equal to the product of `m` cast to a `Nat` and `n` cast to a `Nat`. In mathematical terms, for all `m` and `n`, `(m * n)` cast to a natural number is equal to `(m` cast to a natural number`) * (n` cast to a natural number`).
More concisely: For all natural numbers `m` and `n`, `(m : Nat) * n = m * (n : Nat)`.
|
ZNum.cast_to_int
theorem ZNum.cast_to_int : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑↑n = ↑n
This theorem states that, for every type `α` (which must be an instance of an additive group with a multiplicative identity), the double cast of a ZNum `n` to `α` is equal to the single cast of `n` to `α`. In other words, the double application of the coercion function (cast operation) to `n` does not change the result from the single application of the coercion function.
More concisely: For any additive group type `α`, the double coercion of a ZNum `n` to `α` equals the single coercion of `n` to `α`.
|
Num.zneg_toZNumNeg
theorem Num.zneg_toZNumNeg : ∀ (n : Num), -n.toZNumNeg = n.toZNum
The theorem `Num.zneg_toZNumNeg` states that for every number of type `Num`, the negation of the result of the function `toZNumNeg` applied to the number is equal to the result of the function `toZNum` applied to the same number. In other words, for all natural numbers `n`, negating the conversion of `n` to a negative `ZNum` yields the same result as directly converting `n` to a `ZNum`.
More concisely: For every natural number `n`, `toZNum (toZNumNeg n)` equals `toZNumNeg n`.
|
Num.succ'_to_nat
theorem Num.succ'_to_nat : ∀ (n : Num), ↑n.succ' = ↑n + 1
This theorem states that for any natural number `n`, the natural number representation of the successor of `n` (denoted as `Num.succ' n`) is equal to the sum of the natural number representation of `n` and 1. In other words, applying the function `Num.succ'` to a number `n` and then converting to a natural number yields the same result as first converting `n` to a natural number and then adding 1.
More concisely: For all natural numbers `n`, `Num.succ' n = n + 1`.
|
ZNum.cast_pos
theorem ZNum.cast_pos :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : PosNum),
↑(ZNum.pos n) = ↑n
This theorem, `ZNum.cast_pos`, states that for any positive number `n` of type `PosNum`, its casting as `ZNum.pos n` is equal to its casting as `n`. Here, `α` is any type with zero, one, addition, and negation operations defined. In mathematical terms, it says that casting a positive integer `n` from the `PosNum` type to the `ZNum` type doesn't change its value.
More concisely: For any positive number `n` of type `PosNum`, the cast `ZNum.pos n` is equal to `n`.
|
PosNum.cast_one
theorem PosNum.cast_one : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α], ↑1 = 1
This theorem states that for any type `α` that has both the identity element for addition (`One α`) and the addition operation (`Add α`), the casting of the positive number one (`1`) into type `α` is equal to the identity element `1` of type `α`. Essentially, it is confirming that the casting operation correctly identifies the number one in other mathematical structures that have a concept equivalent to 'one'.
More concisely: For any type `α` with an addition operation and an identity element, the cast of `1` to `α` equals the identity element.
|
PosNum.cmp_to_nat
theorem PosNum.cmp_to_nat : ∀ (m n : PosNum), Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
The theorem `PosNum.cmp_to_nat` is a statement about positive numbers (`PosNum`) in Lean 4. It says that for all positive numbers `m` and `n`, when we compare `m` and `n` using the `PosNum.cmp` function, the resulting ordering matches the natural number comparison (`<`, `=`, or `>`). Specifically, if `PosNum.cmp m n` results in `Ordering.lt`, then `m` as a natural number is less than `n` as a natural number (denoted by `↑m < ↑n`). If `PosNum.cmp m n` results in `Ordering.eq`, then `m` is equal to `n`. If `PosNum.cmp m n` results in `Ordering.gt`, then `n` as a natural number is less than `m` as a natural number (denoted by `↑n < ↑m`).
More concisely: For all positive numbers `m` and `n`, `PosNum.cmp m n` orders `m` and `n` consistently with the natural number comparison, that is, `m < n` if and only if `PosNum.cmp m n` is `Ordering.lt`, `m = n` if and only if `PosNum.cmp m n` is `Ordering.eq`, and `n < m` if and only if `PosNum.cmp m n` is `Ordering.gt`.
|
PosNum.add_one
theorem PosNum.add_one : ∀ (n : PosNum), n + 1 = n.succ
The theorem `PosNum.add_one` states that for every positive number `n`, the result of adding 1 to `n` is the same as the successor of `n`. In other words, it formalizes the common arithmetic property that adding one to any positive number results in its next consecutive number. The successor function is defined in such a way that it extends the positive numbers to include `PosNum.one` (for 1), `PosNum.bit0 n` (for even numbers), and `PosNum.bit1 n` (for odd numbers).
More concisely: For every positive number `n`, `1 + n` equals the successor of `n`.
|
Num.to_nat_to_int
theorem Num.to_nat_to_int : ∀ (n : Num), ↑↑n = ↑n
This theorem states that for every numeral `n`, the process of first converting `n` to a natural number (`to_nat`) and then converting the result to an integer (`to_int`) is the same as directly converting `n` to an integer. In other words, the two conversions are equivalent for each numeral.
More concisely: For every numeral `n`, the conversion of `n` to an integer is equivalent to first converting `n` to a natural number and then converting the result to an integer.
|
ZNum.add_one
theorem ZNum.add_one : ∀ (n : ZNum), n + 1 = n.succ
This theorem states that for any given integer number `n` represented as `ZNum` in Lean 4, incrementing `n` by `1` is equivalent to the successor of `n` (`ZNum.succ n`). The successor operation in this context is defined such that the successor of zero is 1, the successor of a positive number is the next positive number, and the successor of a negative number is the previous negative number.
More concisely: For any integer `n` in Lean 4, `ZNum.succ n` is equal to the integer obtained by adding 1 to `n`.
|
Num.add_to_nat
theorem Num.add_to_nat : ∀ (m n : Num), ↑(m + n) = ↑m + ↑n
This theorem states that for all numbers `m` and `n` of the `Num` type, the coercion of the sum of `m` and `n` to a natural number is equal to the sum of the individual coercions of `m` and `n` to natural numbers. In mathematical terms, this theorem is saying that for any `m` and `n` in `Num`, `(m + n) ⟶ ℕ = m ⟶ ℕ + n ⟶ ℕ`.
More concisely: The coercion of the sum of two numbers is equal to the sum of their individual coercions to natural numbers. In Lean notation, this is expressed as (m + n) ⟶ ℕ = m ⟶ ℕ + n ⟶ ℕ.
|
PosNum.pred'_to_nat
theorem PosNum.pred'_to_nat : ∀ (n : PosNum), ↑n.pred' = (↑n).pred
This theorem, `PosNum.pred'_to_nat`, establishes a relationship between the predecessor function on positive numbers (`PosNum.pred'`) and the predecessor function on natural numbers (`Nat.pred`). It states that for any positive number `n`, the natural number corresponding to the predecessor of `n` (denoted as `↑(PosNum.pred' n)`) is equal to the predecessor of the natural number corresponding to `n` (denoted as `Nat.pred ↑n`). In other words, applying `PosNum.pred'` to a positive number and then converting to a natural number gives the same result as first converting the positive number to a natural number and then applying `Nat.pred`.
More concisely: For any positive number `n`, `Nat.pred (↑n)` equals `↑(PosNum.pred' n)`.
|
ZNum.mul_to_int
theorem ZNum.mul_to_int : ∀ (m n : ZNum), ↑(m * n) = ↑m * ↑n
This theorem states that for all ZNum numbers `m` and `n`, the operation of casting the product of `m` and `n` to an integer is the same as individually casting `m` and `n` to integers and then multiplying them. In mathematical terms, for all `m` and `n` in ZNum, `(m * n)` casted to an integer is equal to `(m casted to an integer) * (n casted to an integer)`.
More concisely: For all `m` and `n` in ZNum, the integer cast of `(m * n)` equals the product of the integer casts of `m` and `n`.
|
Num.castNum_eq_bitwise
theorem Num.castNum_eq_bitwise :
∀ {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num),
g false false = false →
f 0 0 = 0 →
(∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0) →
(∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0) →
(∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) →
(p 1 1 = bif g true true then 1 else 0) →
(∀ (b : Bool) (n : PosNum),
p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)) →
(∀ (a : Bool) (m : PosNum),
p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)) →
(∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) →
∀ (m n : Num), ↑(f m n) = Nat.bitwise g ↑m ↑n
This theorem, `Num.castNum_eq_bitwise`, states that for any two Num-to-Num functions `f` and `g`, and a PosNum-to-PosNum-to-Num function `p`, given certain conditions, the cast of the application of `f` to any two Num values `m` and `n` is equal to the bitwise operation on the cast of `m` and `n` using `g`.
The conditions for this to hold are:
- `g` returns `false` when applied to two `false` Boolean values,
- `f` returns `0` when applied to two `0` Num values,
- For any positive number `n`, `f` returns `Num.pos n` if `g` applied to `false` and `true` returns `true`, and `0` otherwise,
- Similar condition holds for `f` returning `Num.pos n` if `g` applied to `true` and `false` returns `true`, and `0` otherwise, for any positive number `n`,
- For any two positive numbers `m` and `n`, `f` returns the application of `p` to `m` and `n`,
- `p` returns `1` if `g` applied to two `true` Boolean values returns `true`, and `0` otherwise,
- For any Boolean value `b` and positive number `n`, `p` returns the bitwise operation on `g` applied to `true` and `b` and `Num.pos n` if `g` applied to `false` and `true` returns `true`, and `0` otherwise,
- A similar condition holds for `p` returning the bitwise operation on `g` applied to `a` and `true` and `Num.pos m` if `g` applied to `true` and `false` returns `true`, and `0` otherwise, for any Boolean value `a` and positive number `m`,
- For any two Boolean values `a` and `b`, and positive numbers `m` and `n`, `p` returns the bitwise operation on `g` applied to `a` and `b` and the application of `p` to `m` and `n`.
These conditions provide a detailed relationship between the behaviour of functions `f`, `g`, and `p` and the bitwise operations.
More concisely: For functions `f`, `g`, and `p` satisfying certain conditions, the cast of `f` applied to two numbers `m` and `n` is equal to the bitwise operation on the casts of `m` and `n` using `g`, represented by `p`.
|
Num.cast_zero
theorem Num.cast_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α], ↑0 = 0
This theorem, named `Num.cast_zero`, states that for any type `α` which has zero `0`, one `1`, and the operation of addition `+` defined, the numeric cast of `0` (from the built-in number type to `α`) is equal to the zero of `α`. In simpler words, casting `0` to any number type that has the concepts of zero, one, and addition will give you the zero in that number type.
More concisely: For any type `α` with zero `0`, one `1`, and addition `+`, the numeric cast of `0` to `α` equals `0` in `α`.
|
PosNum.mul_to_nat
theorem PosNum.mul_to_nat : ∀ (m n : PosNum), ↑(m * n) = ↑m * ↑n
This theorem states that for all positive numbers `m` and `n`, the natural number equivalent of the product of `m` and `n` is equal to the product of the natural number equivalents of `m` and `n`. In other words, multiplication in the domain of positive numbers and then conversion to natural numbers preserves the same result as conversion to natural numbers first and then multiplication.
More concisely: For all positive integers m and n, the conversion of m \* n to natural numbers is equal to the natural number equivalent of m multiplied by the natural number equivalent of n.
|
PosNum.succ'_pred'
theorem PosNum.succ'_pred' : ∀ (n : PosNum), n.pred'.succ' = n
This theorem states that for every positive number 'n', the successor of the predecessor of 'n' is 'n' itself. Here, the successor and predecessor functions are defined for types `Num` (which includes zero and positive numbers) and `PosNum` (which includes only positive numbers), respectively. In mathematical terms, it means for all positive numbers 'n', `n = succ(pred(n))`, where `succ` and `pred` are functions that get the successor and the predecessor of a number, respectively. This theorem essentially ensures the correctness of these functions in the context of positive numbers.
More concisely: For every positive number 'n', the predecessor of its successor is 'n' itself. (Or, more mathematically, `pred(succ(n)) = n` for all positive numbers 'n'.).
|
Num.cast_to_nat
theorem Num.cast_to_nat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : Num), ↑↑n = ↑n
This theorem, `Num.cast_to_nat`, states that for any type `α` which is an additive monoid with a distinct one (i.e., it supports an addition operation and has an element identified as one), the double cast from an instance of the `Num` type to `α` through a natural number (notated as `↑↑n`) is equivalent to a direct cast from `Num` to `α` (notated as `↑n`). Essentially, it assures that the intermediate casting step to a natural number doesn't alter the final result of the cast.
More concisely: For any additive monoid with a distinct one `α` and instance of `Num`, the double cast from `Num` to `α` through a natural number is equal to a direct cast from `Num` to `α`.
|
Num.lt_to_nat
theorem Num.lt_to_nat : ∀ {m n : Num}, ↑m < ↑n ↔ m < n
This theorem states that for any two numbers `m` and `n` of the `Num` type, the statement "the natural number equivalent of `m` is less than the natural number equivalent of `n`" is equivalent to the statement "`m` is less than `n`". In other words, the '<' operator behaves consistently when comparing natural number equivalents of `Num` type numbers.
More concisely: The theorem asserts that for all natural numbers `m` and `n` of type `Num`, `m < n` is equivalent to `to_nat m < to_nat n`, where `to_nat` is the natural number representation function.
|
ZNum.cast_zneg
theorem ZNum.cast_zneg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : One α] (n : ZNum), ↑(-n) = -↑n
This theorem, `ZNum.cast_zneg`, states that for any type `α`, where `α` is an additive group and has an identity element under multiplication, if `n` is a number of type `ZNum` (signed integers), then the negation of `n` cast to type `α` is equal to the negation of `n` cast to type `α`. In other words, casting doesn't change the relationship between `-n` and `n`: if you negate `n` first and then cast, you get the same result as if you cast `n` first and then negate.
More concisely: For any additive group type `α` with identity multiplication, the operation of casting `ZNum` signed integers to `α` preserves negation: `-(CAST α n) = CAST α (-n)`.
|
ZNum.zneg_zneg
theorem ZNum.zneg_zneg : ∀ (n : ZNum), - -n = n
This theorem states that for any integer number `n` (represented as `ZNum` in Lean), the double negation of `n` is equal to `n` itself. In mathematical terms, if `n` is any integer, then the expression `--n = n` is always true.
More concisely: For any integer `n`, the double negation of `n` equals `n` (i.e., `--n = n`).
|
ZNum.to_int_inj
theorem ZNum.to_int_inj : ∀ {m n : ZNum}, ↑m = ↑n ↔ m = n
This theorem states that for any two `ZNum` numbers `m` and `n`, the statement that their integer equivalents (obtained by using the `↑` coercion operator) are equal is logically equivalent to the statement that `m` and `n` themselves are equal. In other words, mapping `ZNum` numbers to integers preserves uniqueness - no two different `ZNum` numbers will map to the same integer.
More concisely: For all `m` and `n` in `ZNum`, `m = n` if and only if `↑m = ↑n`.
|
ZNum.cast_zero
theorem ZNum.cast_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α], ↑0 = 0
This theorem states that for any type `α` which has defined instances of `Zero`, `One`, `Add`, and `Neg`, the cast of the zero integer `0` to type `α` is equal to the zero element of type `α`. This essentially guarantees that the zero integer in the ZNum number system translates to the zero element in any other number system that has a concept of zero, one, addition, and negation.
More concisely: For any type `α` with defined instances of `Zero`, `One`, `Add`, and `Neg`, the conversion of the integer zero to type `α` equals the zero element of `α`.
|
PosNum.succ_to_nat
theorem PosNum.succ_to_nat : ∀ (n : PosNum), ↑n.succ = ↑n + 1
The theorem `PosNum.succ_to_nat` states that for every positive number `n`, the natural number representation of the successor of `n` is equal to the natural number representation of `n` plus one. In other words, it asserts that the `succ` operation on positive numbers corresponds to incrementing by one in the natural numbers.
More concisely: For every positive number `n`, the natural number representation of `n.succ` is one more than the natural number representation of `n`.
|
Num.add_one
theorem Num.add_one : ∀ (n : Num), n + 1 = n.succ
This theorem states that for any natural number `n`, adding one to `n` is equivalent to the successor of `n`. In other words, for any number `n`, `n + 1` is the same as the next number after `n` in the sequence of natural numbers. This is a fundamental property of natural numbers in the Peano postulates.
More concisely: For any natural number `n`, `n + 1` is the same as the successor of `n`. (Alternatively: The successor of a natural number `n` is `n + 1`.)
|
PosNum.le_to_nat
theorem PosNum.le_to_nat : ∀ {m n : PosNum}, ↑m ≤ ↑n ↔ m ≤ n
This theorem states that for all positive numbers `m` and `n`, the equality `m ≤ n` holds if and only if the same inequality holds when both numbers are converted to natural numbers. In other words, a positive number `m` is less than or equal to another positive number `n` if and only if the natural number representation of `m` is less than or equal to the natural number representation of `n`.
More concisely: For all positive integers m and n, m ≤ n if and only if the natural numbers representing m and n satisfy the same inequality.
|
PosNum.to_nat_inj
theorem PosNum.to_nat_inj : ∀ {m n : PosNum}, ↑m = ↑n ↔ m = n
This theorem, `PosNum.to_nat_inj`, states that for any two positive numbers `m` and `n`, the coercion (conversion) of `m` and `n` to natural numbers results in equal natural numbers if and only if `m` and `n` themselves are equal. That is, the process of converting positive numbers to natural numbers preserves their distinctness; no two different positive numbers will become the same natural number after conversion.
More concisely: The coercion of positive numbers to natural numbers is an injection. That is, distinct positive numbers map to distinct natural numbers.
|
PosNum.bit0_of_bit0
theorem PosNum.bit0_of_bit0 : ∀ (n : PosNum), bit0 n = n.bit0
This theorem states that for every positive number `n`, the operation `bit0` applied to `n` is equal to the operation `PosNum.bit0` applied to the same `n`. In other words, the `bit0` operation, which doubles an input value, performs the same operation as `PosNum.bit0` when the input is a positive number.
More concisely: For all positive numbers `n`, `bit0 n` equals `PosNum.bit0 n`.
|
Num.ofNat'_zero
theorem Num.ofNat'_zero : Num.ofNat' 0 = 0
The theorem `Num.ofNat'_zero` states that when the function `Num.ofNat'`, which converts a natural number (`Nat`) to a numerical value (`Num`), is applied to the natural number zero, it returns the numerical value zero. This function uses a binary recursive method to compute the corresponding `Num` value of a `Nat` value.
More concisely: The theorem `Num.ofNat'_zero` asserts that `Num.ofNat' 0 = 0`.
|
Num.to_of_nat
theorem Num.to_of_nat : ∀ (n : ℕ), ↑↑n = n
This theorem states that for every natural number `n`, the double coercion of `n` is equal to `n` itself. Here, coercion is a way in Lean 4 to automatically convert a value from one type to another. So this theorem is essentially saying that converting a natural number to another type (most likely the type of numbers `Num`) and back to a natural number leaves the original number unchanged.
More concisely: For every natural number `n`, the double application of the coercion from `Nat` to some type `Num` and back to `Nat` results in the original number `n`. In mathematical notation: `coercion (coercion n : Num) = n`.
|
PosNum.add_to_nat
theorem PosNum.add_to_nat : ∀ (m n : PosNum), ↑(m + n) = ↑m + ↑n
This theorem states that for all positive numbers `m` and `n`, the natural number representation of the sum of `m` and `n` is equal to the sum of the natural number representations of `m` and `n`. In mathematical terms, given any two positive numbers `m` and `n`, the operation of addition in the domain of positive numbers and its corresponding operation in the domain of natural numbers are preserved under the embedding from positive numbers to natural numbers.
More concisely: For all positive numbers m and n, the natural number representation of m + n equals the sum of the natural number representations of m and n.
|
ZNum.cast_neg
theorem ZNum.cast_neg :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : PosNum),
↑(ZNum.neg n) = -↑n
This theorem, `ZNum.cast_neg`, states that for any type `α` that has defined operations for zero, one, addition, and negation, and for any positive number `n`, the casting of the negation of `n` to `ZNum` (integer number) is equal to the negation of the casting of `n` to `α`. In other words, it ensures that the negation operation works as expected when moving between different numeric types.
More concisely: For any type `α` with zero, one, addition, and negation operations, and for any `n` of type `α`, the cast of `-n` to `ZNum` equals `-(cast n to ZNum)`.
|