AddCommGroupWithOne.natCast_succ
theorem AddCommGroupWithOne.natCast_succ :
∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
This theorem states that for any type `R` that is an additive commutative group with a defined 'one' (`AddCommGroupWithOne R`), the canonical map from natural numbers `ℕ` to `R` (`NatCast.natCast`) preserves the operation of addition. More specifically, it states that casting the natural number `n + 1` to `R` is the same as casting `n` to `R` and then adding one in `R`. This preservation property establishes `NatCast.natCast` as a homomorphism.
More concisely: For any additive commutative group with a one `R`, the natural number casting map `NatCast.natCast : ℕ → R` is a homomorphism, i.e., `NatCast.natCast (n + m) = NatCast.natCast n + NatCast.natCast m`.
|
AddCommGroupWithOne.intCast_ofNat
theorem AddCommGroupWithOne.intCast_ofNat :
∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), IntCast.intCast ↑n = ↑n
This theorem states that for any type `R` that forms an additive commutative group with a distinguished one element, and for any natural number `n`, the standard mapping from the integers `ℤ` to `R` applied to the natural number `n` treated as an integer (using ↑n to denote the coercion or casting of `n` from `ℕ` to `ℤ`), is equal to the direct mapping of `n` to `R`. In other words, when we map a natural number to `R` either directly or via the integers, we get the same result.
More concisely: For any additive commutative group with unity `R` and natural number `n`, the mapping of `n` to `R` via the integers is equal to the direct mapping of `n` to `R`.
|
AddGroupWithOne.intCast_ofNat
theorem AddGroupWithOne.intCast_ofNat : ∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ), IntCast.intCast ↑n = ↑n := by
sorry
This theorem states that for any type `R` that has an associated `AddGroupWithOne` structure, the canonical homomorphism function from integers (`ℤ`) to `R` agrees with the one from natural numbers (`ℕ`) to `R` when applied to any natural number `n`. In other words, if you cast a natural number `n` to an integer and then apply the `IntCast.intCast` function, you get the same result as if you directly cast `n` to `R`.
More concisely: For any type `R` with an `AddGroupWithOne` structure, the integer and natural number homomorphisms from `ℤ` and `ℕ` to `R` agree.
|
AddGroupWithOne.intCast_negSucc
theorem AddGroupWithOne.intCast_negSucc :
∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
The theorem `AddGroupWithOne.intCast_negSucc` states that for any type `R` that forms an additive group with one element and for any natural number `n`, the canonical homomorphism (mapping) from the integers to `R` applied on the negative successor of `n` is equal to the negation of the canonical homomorphism from the natural numbers to `R` applied on `n + 1`. The negative successor of a number in this context represents the number obtained by decrementing it by one. Essentially, this theorem establishes a relationship between the negative integers and natural numbers through their respective homomorphisms to an arbitrary type `R`.
More concisely: For any additive group with one element R and natural number n, the homomorphism from integers to R mapping negative successor of n is equal to the negation of the homomorphism from natural numbers to R mapping n + 1.
|
AddCommGroupWithOne.intCast_negSucc
theorem AddCommGroupWithOne.intCast_negSucc :
∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
The theorem `AddCommGroupWithOne.intCast_negSucc` states that for any type `R` that forms an additive commutative group with a distinguished "one" element, and for any natural number `n`, the canonical homomorphism from the integers `ℤ` to `R` applied to the negation of the successor of `n` is equal to the negation of the canonical homomorphism from the natural numbers `ℕ` to `R` applied to `n + 1`. Essentially, this theorem describes how the mapping from integers to `R` behaves for negative integers in relation to the map from natural numbers to `R`.
More concisely: For any additive commutative group with a multiplicative identity `R` and the canonical homomorphism `int : ℤ → R` from integers to `R`, `int(-(n + 1)) = -int(n + 1)` for all natural numbers `n` in `ℕ`.
|
AddCommGroupWithOne.natCast_zero
theorem AddCommGroupWithOne.natCast_zero : ∀ {R : Type u} [self : AddCommGroupWithOne R], NatCast.natCast 0 = 0 := by
sorry
The theorem `AddCommGroupWithOne.natCast_zero` states that for any type `R` that has an additive commutative group structure with an identity element, the canonical mapping from the natural numbers (`ℕ`) to `R` sends the natural number `0` to the equivalent `0` in `R`. This theorem is foundational to ensuring that the basic properties of natural numbers carry over to other numeric types in a consistent manner.
More concisely: For any additive commutative group with an identity element R, the natural number 0 maps to 0 under the canonical homomorphism from ℕ to R.
|