Int.cast_one
theorem Int.cast_one : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑1 = 1
This theorem states that for any type `R` that is an instance of the `AddGroupWithOne` typeclass, casting the integer `1` to `R` results in `1` in `R`. The `AddGroupWithOne` typeclass is a type that has both addition and `1` as an identity element for multiplication. Thus, this theorem is essentially stating that the identity element for multiplication in the integers (`1`) is the same as the identity element for multiplication in any additive group with an identity for multiplication (`1`).
More concisely: For any additive group with identity element for multiplication `R`, the conversion of the integer `1` to `R` equals the multiplicative identity `1` in `R`.
|
Nat.cast_pred
theorem Nat.cast_pred : ∀ {R : Type u} [inst : AddGroupWithOne R] {n : ℕ}, 0 < n → ↑(n - 1) = ↑n - 1
This theorem states that for any natural number `n` and any type `R` that forms an additive group with one, if `n` is greater than zero, then casting (`↑`) `n - 1` to the type `R` is equal to subtracting one from the cast of `n`. In other words, for positive natural numbers, subtracting one before or after casting to the type `R` yields the same result.
More concisely: For any additive group type `R` with one and natural number `n` greater than zero, casting `n - 1` to `R` is equal to subtracting one from the cast of `n`, i.e., `(↑ (n - 1)) = (↑ n) - 1` in `R`.
|
Mathlib.Data.Int.Cast.Basic._auxLemma.4
theorem Mathlib.Data.Int.Cast.Basic._auxLemma.4 : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℤ), -↑n = ↑(-n) := by
sorry
This theorem, named `Mathlib.Data.Int.Cast.Basic._auxLemma.4`, states that for all types `R` that form an Additive Group with a multiplicative identity (also known as a `AddGroupWithOne`), the negation of the cast of an integer `n` to type `R` is equal to the cast of the negation of `n` to type `R`. In mathematical terms, the theorem says that for any integer `n` and any `R` in the class of add groups with one, `-cast(n) = cast(-n)`.
More concisely: For any additive group with a multiplicative identity `R`, the cast of the negative of an integer to `R` is equal to the negative of the cast of the integer to `R`. In other words, `cast(-n) = -cast(n)` for all integers `n` and additive groups with a multiplicative identity `R`.
|
Mathlib.Data.Int.Cast.Basic._auxLemma.7
theorem Mathlib.Data.Int.Cast.Basic._auxLemma.7 :
∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑m + ↑n = ↑(m + n)
This theorem states that for any type `R` that is an additive group with an identity element, and for any integers `m` and `n`, the cast of the sum of `m` and `n` to `R` is equal to the sum of the casts of `m` and `n` to `R`. In mathematical terms, it states that for every `m` and `n` in the set of integers ℤ, the equation `↑m + ↑n = ↑(m + n)` holds true, where `↑m` and `↑n` represent the casting of the integers `m` and `n` to the type `R`.
More concisely: For any additive group `R` with identity and integers `m` and `n`, the cast of their sum to `R` equals the cast of each integer followed by their addition: `↑(m + n) = ↑m + ↑n`.
|
Int.cast_sub
theorem Int.cast_sub : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m - n) = ↑m - ↑n
This theorem, `Int.cast_sub`, states that for any type `R` that is an instance of `AddGroupWithOne` (meaning it is a mathematical group that has addition as its operation and contains an identity element) and for any two integers `m` and `n`, the result of casting the difference between `m` and `n` (i.e., `m - n`) to type `R` is equal to the difference of `m` and `n` as `R` (cast individually and then subtracted). Simply put, the casting operation respects subtraction for `AddGroupWithOne` instances.
More concisely: For any `AddGroupWithOne` type `R` and integers `m` and `n`, the operation `(m : R) - (n : R)` equals `(m : R) -^ (n : R)`, where `-` is subtraction on integers and `-^` is subtraction on type `R`.
|
Int.cast_add
theorem Int.cast_add : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m + n) = ↑m + ↑n
This theorem, `Int.cast_add`, states that for any type `R` that forms an additive group with an identity element, the cast of the sum of two integers `m` and `n` into `R` is equal to the sum of the individual casts of `m` and `n` into `R`. In other words, the operation of casting an integer into another type commutes with the addition operation on integers. This is a fundamental property of addition that allows for more flexible and powerful mathematical manipulations.
More concisely: For any additive group `R` with identity element, the cast of `m + n` into `R` is equal to the cast of `m` into `R` plus the cast of `n` into `R`. (In Lean notation: `to_add R m n = to_add R m (to_add R n)`)
|
Int.cast_ofNat
theorem Int.cast_ofNat :
∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n := by
sorry
This theorem states that for any natural number 'n', the two-step integer casting of 'n' to a type 'R' (which has 'AddGroupWithOne' structure) is the same as the single-step casting of 'n' to 'R'. In other words, if you first cast a natural number to an integer, and then cast that integer to a type 'R' (which is an additive group with an identity element), it's the same as if you cast the natural number directly to 'R'.
More concisely: For any natural number n, the two-step casting of n to an additive group with an identity element R is equal to the single-step casting of n to R.
|
Int.cast_zero
theorem Int.cast_zero : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑0 = 0
This theorem states that for any type `R` that forms an additive group with an identity element (specifically, a structure that complies with the `AddGroupWithOne` typeclass in Lean), the casting of the integer zero `↑0` into type `R` is equal to the zero of type `R`. Essentially, it guarantees that zero maintains its identity when cast to different types that have a notion of zero and a specified algebraic structure.
More concisely: For any additive group `R` with identity element, the cast of integer zero `↑0` is equal to the additive identity of `R`.
|
Nat.cast_sub
theorem Nat.cast_sub : ∀ {R : Type u} [inst : AddGroupWithOne R] {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
This theorem states that for all types `R` that form an additive group with a unit element (which means `R` has operations for addition, zero, negation, and one), and for all natural numbers `m` and `n` where `m` is less than or equal to `n`, the cast of the subtraction of `m` from `n` (`n - m`) to `R` is equal to the subtraction of the cast of `m` to `R` from the cast of `n` to `R` (`↑n - ↑m`). Essentially, this captures the idea that casting doesn't interfere with subtraction: the order of casting and subtraction can be swapped without changing the result.
More concisely: For all additive groups `R` with unit and natural numbers `m ≤ n`, the cast of `n - m` to `R` equals the cast of `n` to `R` minus the cast of `m` to `R` (i.e., `↑(n - m) = ↑n - ↑m`).
|
Int.cast_neg
theorem Int.cast_neg : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℤ), ↑(-n) = -↑n
This theorem, `Int.cast_neg`, states that for every integer `n`, the negation of `n` cast into an arbitrary type `R` (that is, `-n` as an element of `R`), is equal to the negation of `n` as an element of `R`. Here, the type `R` is assumed to be an addable group with a unity (which typically means there's a zero, a negative operation, an addition operation, and a "one" element defined in a compatible way on `R`). In mathematical notation, this could be expressed as ∀n ∈ ℤ, ∀R ∈ AddGroupWithOne, cast(-n) = -cast(n).
More concisely: For every integer `n` and additive group with unity `R`, the negation of the integer `n` cast to `R` equals the negation of `n` as an element of `R`. In mathematical notation: ∀n ∈ ℤ, ∀R ∈ AddGroupWithOne, -cast(n) = cast(-n).
|
Mathlib.Data.Int.Cast.Basic._auxLemma.3
theorem Mathlib.Data.Int.Cast.Basic._auxLemma.3 :
∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ), -↑(n + 1) = ↑(Int.negSucc n)
This theorem states that for any natural number `n` and any type `R` that forms an additive group with a distinguished one, the negation of the cast of `n + 1` is the same as the cast of `Int.negSucc n`. In terms of mathematical notation, this is saying that for all natural numbers `n` and any `R` in the AddGroupWithOne, `-↑(n + 1) = ↑(Int.negSucc n)`. The `Int.negSucc` function gives the negative of the successor (or next) integer, so this theorem essentially asserts a property about negations and successors in additive groups with a distinguished one.
More concisely: For any natural number `n` and additive group `R` with one, the negation of `n + 1` in `R` equals the additive inverse of `n` in `R`.
|
Mathlib.Data.Int.Cast.Basic._auxLemma.8
theorem Mathlib.Data.Int.Cast.Basic._auxLemma.8 :
∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑m - ↑n = ↑(m - n)
This theorem states that for any type `R` that has a structure of an additive group with a multiplicative identity (i.e., `AddGroupWithOne R`), and for any two integers `m` and `n`, the difference of the casted integers `m` and `n` in `R` is equal to the cast of the difference of the integers `m` and `n`. In mathematical terms, this can be represented as $(m - n) = [m] - [n]$, where $[m]$ and $[n]$ represent the casted integers.
More concisely: For any additive group with a multiplicative identity `R` and integers `m` and `n`, the casted integers `[m]` and `[n]` differ by the group difference `m - n`.
|
Int.cast_negSucc
theorem Int.cast_negSucc : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ), ↑(Int.negSucc n) = -↑(n + 1)
The theorem `Int.cast_negSucc` states that for any type `R` which forms an additive group with a distinguished one element, and for any natural number `n`, the casting of the negative successor of `n` (in the integers) to `R` is equal to the negation of the result of casting `n+1` to `R`. In other words, it formalizes our intuitive understanding of negation and successor operations across different numerical types.
More concisely: For any additive group type R and natural number n, the casting of the negative successor of n to R equals the additive inverse of the casting of n+1 to R.
|
Mathlib.Data.Int.Cast.Basic._auxLemma.1
theorem Mathlib.Data.Int.Cast.Basic._auxLemma.1 :
∀ {R : Type u} [inst : AddGroupWithOne R] {m n : ℕ}, m ≤ n → ↑n - ↑m = ↑(n - m)
This theorem states that for any type `R` which is an instance of the `AddGroupWithOne` type class, and any two natural numbers `m` and `n` where `m` is less than or equal to `n`, the difference of the cast of `n` and the cast of `m` in `R` is equal to the cast of the difference of `n` and `m` in `R`. In mathematical terms, it asserts that for `m ≤ n`, `(↑n - ↑m) = ↑(n - m)`, where the ↑ symbol denotes the casting operation.
More concisely: For any type `R` an instance of `AddGroupWithOne` and natural numbers `m ≤ n`, `(↑n - ↑m) = ↑(n - m)`.
|