doc-next-gen

Mathlib.Data.Int.Cast.Basic

Module docstring

{"# Cast of integers (additional theorems)

This file proves additional properties about the canonical homomorphism from the integers into an additive group with a one (Int.cast).

There is also Data.Int.Cast.Lemmas, which includes lemmas stated in terms of algebraic homomorphisms, and results involving the order structure of ℤ.

By contrast, this file's only import beyond Data.Int.Cast.Defs is Algebra.Group.Basic. "}

Nat.cast_sub theorem
{m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m
Full source 
@[simp, norm_cast]
theorem cast_sub {m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m :=
  eq_sub_of_add_eq <| by rw [← cast_add, Nat.sub_add_cancel h]
Canonical Homomorphism Preserves Subtraction: $\text{cast}(n - m) = \text{cast}(n) - \text{cast}(m)$ for $m \leq n$
Informal description
For any additive group with one $R$ and natural numbers $m$ and $n$ such that $m \leq n$, the canonical homomorphism from $\mathbb{N}$ to $R$ satisfies $\text{cast}(n - m) = \text{cast}(n) - \text{cast}(m)$.
Nat.cast_pred theorem
: ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1
Full source 
@[simp, norm_cast]
theorem cast_pred : ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1
  | 0, h => by cases h
  | n + 1, _ => by rw [cast_succ, add_sub_cancel_right]; rfl
Canonical Homomorphism Preserves Predecessor: $\text{cast}(n - 1) = \text{cast}(n) - 1$ for $n > 0$
Informal description
For any natural number $n > 0$ and any additive group with one $R$, the canonical homomorphism from $\mathbb{N}$ to $R$ satisfies $\text{cast}(n - 1) = \text{cast}(n) - 1$.
Int.cast_negSucc theorem
(n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ)
Full source 
@[simp, norm_cast squash]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
  AddGroupWithOne.intCast_negSucc n
Canonical Homomorphism Preserves Negative Successor: $\text{cast}(- [n+1]) = - (n + 1)$
Informal description
For any natural number $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the negative successor $- [n+1]$ to the negation of $(n + 1)$ in $R$, i.e., $\text{cast}(- [n+1]) = - (n + 1)$.
Int.cast_zero theorem
: ((0 : ℤ) : R) = 0
Full source 
@[simp, norm_cast]
theorem cast_zero : ((0 : ℤ) : R) = 0 :=
  (AddGroupWithOne.intCast_ofNat 0).trans Nat.cast_zero
Canonical Homomorphism Preserves Zero: $\text{cast}(0) = 0$ for Integers
Informal description
For any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps $0$ to the additive identity $0$ in $R$, i.e., $\text{cast}(0) = 0$.
Int.cast_natCast theorem
(n : ℕ) : ((n : ℤ) : R) = n
Full source 
@[simp high, nolint simpNF, norm_cast]
theorem cast_natCast (n : ℕ) : ((n : ℤ) : R) = n :=
  AddGroupWithOne.intCast_ofNat _
Coercion of Natural Number as Integer to Additive Group with One
Informal description
For any natural number $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $n$ to the element $n$ in $R$. In other words, the coercion of $n$ from $\mathbb{Z}$ to $R$ equals the element $n$ in $R$.
Int.cast_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℤ) : R) = ofNat(n)
Full source 
@[simp, norm_cast]
theorem cast_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : ℤ) : R) = ofNat(n) := by
  simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n
Coercion of Numerals ≥ 2 from Integers to Additive Group with One
Informal description
For any natural number $n \geq 2$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $n$ to the element $n$ in $R$. In other words, the coercion of $n$ from $\mathbb{Z}$ to $R$ equals the element $n$ in $R$.
Int.cast_one theorem
: ((1 : ℤ) : R) = 1
Full source 
@[simp, norm_cast]
theorem cast_one : ((1 : ℤ) : R) = 1 := by
  rw [← Int.natCast_one, cast_natCast, Nat.cast_one]
Canonical Homomorphism Preserves One: $\text{cast}(1) = 1$
Informal description
For any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $1$ to the multiplicative identity $1$ in $R$, i.e., $\text{cast}(1) = 1$.
Int.cast_neg theorem
: ∀ n, ((-n : ℤ) : R) = -n
Full source 
@[simp, norm_cast]
theorem cast_neg : ∀ n, ((-n : ℤ) : R) = -n
  | (0 : ℕ) => by simp
  | (n + 1 : ℕ) => by rw [cast_natCast, neg_ofNat_succ]; simp
  | -[n+1] => by rw [Int.neg_negSucc, cast_natCast]; simp
Canonical Homomorphism Preserves Negation: $\text{cast}(-n) = -\text{cast}(n)$
Informal description
For any integer $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the negation $-n$ to the negation of $n$ in $R$, i.e., $\text{cast}(-n) = -\text{cast}(n)$.
Int.cast_subNatNat theorem
(m n) : ((Int.subNatNat m n : ℤ) : R) = m - n
Full source 
@[simp, norm_cast]
theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n := by
  unfold subNatNat
  cases e : n - m
  · simp only [ofNat_eq_coe]
    simp [e, Nat.le_of_sub_eq_zero e]
  · rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
Canonical Homomorphism Preserves Subtraction of Natural Numbers: $\text{cast}(\text{subNatNat}(m, n)) = m - n$
Informal description
For any natural numbers $m$ and $n$, and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $\text{subNatNat}(m, n)$ to the difference $m - n$ in $R$, i.e., $\text{cast}(\text{subNatNat}(m, n)) = m - n$.
Int.cast_negOfNat theorem
(n : ℕ) : ((negOfNat n : ℤ) : R) = -n
Full source 
@[simp]
theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n := by simp [Int.cast_neg, negOfNat_eq]
Canonical Homomorphism Maps `negOfNat` to Negation: $\text{cast}(\text{negOfNat}\, n) = -n$
Informal description
For any natural number $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer `negOfNat n` (which represents $-n$ as an integer) to the negation $-n$ in $R$, i.e., $\text{cast}(\text{negOfNat}\, n) = -n$.
Int.cast_add theorem
: ∀ m n, ((m + n : ℤ) : R) = m + n
Full source 
@[simp, norm_cast]
theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n
  | (m : ℕ), (n : ℕ) => by simp [← Int.natCast_add]
  | (m : ℕ), -[n+1] => by erw [cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
  | -[m+1], (n : ℕ) => by
    #adaptation_note
    /-- `_root_` can be removed again after
    https://github.com/leanprover/lean4/pull/7359 lands in nightly-2025-03-06. -/
    erw [cast_subNatNat, cast_natCast, cast_negSucc, _root_.sub_eq_iff_eq_add, add_assoc,
      eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
  | -[m+1], -[n+1] =>
    show (-[m + n + 1+1] : R) = _ by
      rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
        Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
Canonical Homomorphism Preserves Addition: $\text{cast}(m + n) = \text{cast}(m) + \text{cast}(n)$
Informal description
For any integers $m$ and $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ preserves addition, i.e., $(m + n : \mathbb{Z}) : R = m + n$.
Int.cast_sub theorem
(m n) : ((m - n : ℤ) : R) = m - n
Full source 
@[simp, norm_cast]
theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n := by
  simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]
Canonical Homomorphism Preserves Subtraction: $\text{cast}(m - n) = \text{cast}(m) - \text{cast}(n)$
Informal description
For any integers $m$ and $n$ and any additive group with one $R$, the canonical homomorphism from the integers to $R$ preserves subtraction, i.e., $(m - n : \mathbb{Z}) : R = m - n$.
Int.cast_two theorem
: ((2 : ℤ) : R) = 2
Full source 
theorem cast_two : ((2 : ℤ) : R) = 2 := cast_ofNat _
Coercion of Integer 2 to Additive Group with One
Informal description
For any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $2$ to the element $2$ in $R$, i.e., $((2 : \mathbb{Z}) : R) = 2$.
Int.cast_three theorem
: ((3 : ℤ) : R) = 3
Full source 
theorem cast_three : ((3 : ℤ) : R) = 3 := cast_ofNat _
Coercion of Integer 3 to Additive Group with One
Informal description
For any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $3$ to the element $3$ in $R$, i.e., $((3 : \mathbb{Z}) : R) = 3$.
Int.cast_four theorem
: ((4 : ℤ) : R) = 4
Full source 
theorem cast_four : ((4 : ℤ) : R) = 4 := cast_ofNat _
Coercion of Integer 4 to Additive Group with One
Informal description
For any additive group with one $R$, the canonical homomorphism from the integers to $R$ maps the integer $4$ to the element $4$ in $R$, i.e., $((4 : \mathbb{Z}) : R) = 4$.
zsmul_one theorem
[AddGroupWithOne R] (n : ℤ) : n • (1 : R) = n
Full source 
@[simp] lemma zsmul_one [AddGroupWithOne R] (n : ℤ) : n • (1 : R) = n := by cases n <;> simp
Scalar Multiplication of One by Integer: $n \cdot 1 = n$
Informal description
For any additive group with one $R$ and any integer $n$, the scalar multiplication of the multiplicative identity $1 \in R$ by $n$ equals $n$, i.e., $n \cdot 1 = n$.