doc-next-gen

Mathlib.Data.Int.Cast.Lemmas

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), particularly results involving algebraic homomorphisms or the order structure on ℤ which were not available in the import dependencies of Data.Int.Cast.Basic.

Main declarations

  • castAddHom: cast bundled as an AddMonoidHom.
  • castRingHom: cast bundled as a RingHom. "}
Int.ofNatHom definition
: ℕ →+* ℤ
Full source 
/-- Coercion `ℕ → ℤ` as a `RingHom`. -/
def ofNatHom : ℕℕ →+* ℤ :=
  Nat.castRingHom ℤ
Canonical ring homomorphism from naturals to integers
Informal description
The canonical ring homomorphism from the natural numbers $\mathbb{N}$ to the integers $\mathbb{Z}$, which maps each natural number $n$ to the corresponding integer $n$ and preserves addition, multiplication, and the multiplicative identity.
Int.cast_ite theorem
[IntCast α] (P : Prop) [Decidable P] (m n : ℤ) : ((ite P m n : ℤ) : α) = ite P (m : α) (n : α)
Full source 
@[simp, norm_cast]
theorem cast_ite [IntCast α] (P : Prop) [Decidable P] (m n : ℤ) :
    ((ite P m n : ℤ) : α) = ite P (m : α) (n : α) :=
  apply_ite _ _ _ _
Integer Cast Commutes with Conditional Expression
Informal description
For any type $\alpha$ with an integer casting operation, any proposition $P$ with a decision procedure, and any integers $m$ and $n$, the cast of the conditional expression $\text{ite}(P, m, n)$ in $\alpha$ is equal to the conditional expression $\text{ite}(P, (m : \alpha), (n : \alpha))$. In other words, integer casting commutes with conditional expressions: $$(\text{ite}(P, m, n) : \alpha) = \text{ite}(P, (m : \alpha), (n : \alpha))$$
Int.castAddHom definition
(α : Type*) [AddGroupWithOne α] : ℤ →+ α
Full source 
/-- `coe : ℤ → α` as an `AddMonoidHom`. -/
def castAddHom (α : Type*) [AddGroupWithOne α] : ℤℤ →+ α where
  toFun := Int.cast
  map_zero' := cast_zero
  map_add' := cast_add
Canonical additive monoid homomorphism from integers to an additive group with one
Informal description
The bundled additive monoid homomorphism from the integers $\mathbb{Z}$ to an additive group with one $\alpha$, where the underlying function is the canonical homomorphism $\text{Int.cast} : \mathbb{Z} \to \alpha$ that preserves addition and maps zero to zero.
Int.coe_castAddHom theorem
: ⇑(castAddHom α) = fun x : ℤ => (x : α)
Full source 
@[simp] lemma coe_castAddHom : ⇑(castAddHom α) = fun x : ℤ => (x : α) := rfl
Underlying Function of Integer Cast Homomorphism
Informal description
The underlying function of the canonical additive monoid homomorphism `Int.castAddHom` from the integers $\mathbb{Z}$ to an additive group with one $\alpha$ is equal to the function that maps each integer $x$ to its canonical image $(x : \alpha)$ in $\alpha$.
Even.intCast theorem
{n : ℤ} (h : Even n) : Even (n : α)
Full source 
lemma _root_.Even.intCast {n : ℤ} (h : Even n) : Even (n : α) := h.map (castAddHom α)
Preservation of Evenness Under Integer Cast
Informal description
For any integer $n$ and any additive group with one $\alpha$, if $n$ is even, then its image under the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ is also even.
Int.cast_eq_zero theorem
: (n : α) = 0 ↔ n = 0
Full source 
@[simp] lemma cast_eq_zero : (n : α) = 0 ↔ n = 0 where
  mp h := by
    cases n
    · erw [Int.cast_natCast] at h
      exact congr_arg _ (Nat.cast_eq_zero.1 h)
    · rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h
      contradiction
  mpr h := by rw [h, cast_zero]
Characterization of Zero Image in Characteristic Zero Groups: $(n : \alpha) = 0 \leftrightarrow n = 0$
Informal description
For any integer $n$ and any additive group with one $\alpha$ of characteristic zero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ maps $n$ to zero if and only if $n$ is zero, i.e., $(n : \alpha) = 0 \leftrightarrow n = 0$.
Int.cast_inj theorem
: (m : α) = n ↔ m = n
Full source 
@[simp, norm_cast]
lemma cast_inj : (m : α) = n ↔ m = n := by rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
Injectivity of Integer Cast in Characteristic Zero Groups: $(m : \alpha) = (n : \alpha) \leftrightarrow m = n$
Informal description
For any integers $m$ and $n$ and any additive group with one $\alpha$ of characteristic zero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ satisfies $(m : \alpha) = (n : \alpha)$ if and only if $m = n$.
Int.cast_injective theorem
: Injective (Int.cast : ℤ → α)
Full source 
lemma cast_injective : Injective (Int.cast : ℤ → α) := fun _ _ ↦ cast_inj.1
Injectivity of Integer Cast in Characteristic Zero Groups
Informal description
The canonical homomorphism from the integers $\mathbb{Z}$ to an additive group with one $\alpha$ of characteristic zero is injective. That is, for any integers $m, n \in \mathbb{Z}$, if $(m : \alpha) = (n : \alpha)$, then $m = n$.
Int.cast_ne_zero theorem
: (n : α) ≠ 0 ↔ n ≠ 0
Full source 
lemma cast_ne_zero : (n : α) ≠ 0(n : α) ≠ 0 ↔ n ≠ 0 := not_congr cast_eq_zero
Nonzero Preservation under Integer Cast in Characteristic Zero Groups
Informal description
For any integer $n$ and any additive group with one $\alpha$ of characteristic zero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ maps $n$ to a nonzero element if and only if $n$ is nonzero, i.e., $(n : \alpha) \neq 0 \leftrightarrow n \neq 0$.
Int.cast_eq_one theorem
: (n : α) = 1 ↔ n = 1
Full source 
@[simp] lemma cast_eq_one : (n : α) = 1 ↔ n = 1 := by rw [← cast_one, cast_inj]
Characterization of Integer Cast to One: $(n : \alpha) = 1 \leftrightarrow n = 1$
Informal description
For any integer $n$ and any additive group with one $\alpha$ of characteristic zero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ maps $n$ to the multiplicative identity $1$ if and only if $n = 1$, i.e., $(n : \alpha) = 1 \leftrightarrow n = 1$.
Int.cast_ne_one theorem
: (n : α) ≠ 1 ↔ n ≠ 1
Full source 
lemma cast_ne_one : (n : α) ≠ 1(n : α) ≠ 1 ↔ n ≠ 1 := cast_eq_one.not
Non-Identity Preservation under Integer Cast in Characteristic Zero Groups
Informal description
For any integer $n$ and any additive group with one $\alpha$ of characteristic zero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ maps $n$ to an element different from the multiplicative identity $1$ if and only if $n \neq 1$, i.e., $(n : \alpha) \neq 1 \leftrightarrow n \neq 1$.
Int.castRingHom definition
: ℤ →+* α
Full source 
/-- `coe : ℤ → α` as a `RingHom`. -/
def castRingHom : ℤℤ →+* α where
  toFun := Int.cast
  map_zero' := cast_zero
  map_add' := cast_add
  map_one' := cast_one
  map_mul' := cast_mul
Canonical ring homomorphism from integers to a ring
Informal description
The canonical ring homomorphism from the integers $\mathbb{Z}$ to a ring $\alpha$, which maps each integer $n$ to its image under the canonical embedding $\mathbb{Z} \to \alpha$. This homomorphism preserves the additive and multiplicative structures, sending $0$ to $0$, $1$ to $1$, addition to addition, and multiplication to multiplication.
Int.coe_castRingHom theorem
: ⇑(castRingHom α) = fun x : ℤ ↦ (x : α)
Full source 
@[simp] lemma coe_castRingHom : ⇑(castRingHom α) = fun x : ℤ ↦ (x : α) := rfl
Canonical Ring Homomorphism from Integers to a Ring is the Cast Function
Informal description
The canonical ring homomorphism $\text{castRingHom}_\alpha$ from the integers $\mathbb{Z}$ to a ring $\alpha$ is equal to the function that maps each integer $x \in \mathbb{Z}$ to its canonical image $x \in \alpha$.
Int.cast_commute theorem
: ∀ (n : ℤ) (a : α), Commute (↑n) a
Full source 
lemma cast_commute : ∀ (n : ℤ) (a : α), Commute ↑n a
  | (n : ℕ), x => by simpa using n.cast_commute x
  | -[n+1], x => by
    simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
      (n + 1).cast_commute (-x)
Commutativity of Integer Cast with Semiring Elements: $n \cdot a = a \cdot n$
Informal description
For any integer $n$ and any element $a$ in a semiring $\alpha$, the canonical image of $n$ in $\alpha$ commutes with $a$, i.e., $n \cdot a = a \cdot n$.
Int.cast_comm theorem
(n : ℤ) (x : α) : n * x = x * n
Full source 
lemma cast_comm (n : ℤ) (x : α) : n * x = x * n := (cast_commute ..).eq
Commutativity of Integer Cast Multiplication: $n \cdot x = x \cdot n$
Informal description
For any integer $n$ and any element $x$ in a semiring $\alpha$, the product of the canonical image of $n$ in $\alpha$ and $x$ is equal to the product of $x$ and the canonical image of $n$, i.e., $n \cdot x = x \cdot n$.
Int.commute_cast theorem
(a : α) (n : ℤ) : Commute a n
Full source 
lemma commute_cast (a : α) (n : ℤ) : Commute a n := (cast_commute ..).symm
Commutativity of Semiring Element with Integer Cast: $a \cdot n = n \cdot a$
Informal description
For any element $a$ in a semiring $\alpha$ and any integer $n$, the element $a$ commutes with the canonical image of $n$ in $\alpha$, i.e., $a \cdot n = n \cdot a$.
zsmul_eq_mul theorem
(a : α) : ∀ n : ℤ, n • a = n * a
Full source 
@[simp] lemma _root_.zsmul_eq_mul (a : α) : ∀ n : ℤ, n • a = n * a
  | (n : ℕ) => by rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
  | -[n+1] => by simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]
Scalar Multiplication Equals Ring Multiplication: $n \cdot a = n * a$
Informal description
For any element $a$ in a ring $\alpha$ and any integer $n$, the scalar multiplication of $a$ by $n$ equals the product of $n$ and $a$, i.e., $n \cdot a = n * a$.
zsmul_eq_mul' theorem
(a : α) (n : ℤ) : n • a = a * n
Full source 
lemma _root_.zsmul_eq_mul' (a : α) (n : ℤ) : n • a = a * n := by
  rw [zsmul_eq_mul, (n.cast_commute a).eq]
Scalar Multiplication Equals Right Multiplication: $n \cdot a = a * n$
Informal description
For any element $a$ in a ring $\alpha$ and any integer $n$, the scalar multiplication of $a$ by $n$ equals the product of $a$ and $n$, i.e., $n \cdot a = a * n$.
Odd.intCast theorem
(hn : Odd n) : Odd (n : α)
Full source 
lemma _root_.Odd.intCast (hn : Odd n) : Odd (n : α) := hn.map (castRingHom α)
Oddness is preserved under integer ring homomorphism
Informal description
For any integer $n$ and any ring $\alpha$, if $n$ is odd (as an integer), then its image under the canonical ring homomorphism $\mathbb{Z} \to \alpha$ is also odd in $\alpha$.
Int.cast_dvd_cast theorem
[Ring α] (m n : ℤ) (h : m ∣ n) : (m : α) ∣ (n : α)
Full source 
theorem cast_dvd_cast [Ring α] (m n : ℤ) (h : m ∣ n) : (m : α) ∣ (n : α) :=
  RingHom.map_dvd (Int.castRingHom α) h
Divisibility is preserved under integer ring homomorphism
Informal description
Let $\alpha$ be a ring. For any integers $m$ and $n$ such that $m$ divides $n$, the image of $m$ under the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ divides the image of $n$ in $\alpha$.
SemiconjBy.intCast_mul_right theorem
(h : SemiconjBy a x y) (n : ℤ) : SemiconjBy a (n * x) (n * y)
Full source 
@[simp] lemma intCast_mul_right (h : SemiconjBy a x y) (n : ℤ) : SemiconjBy a (n * x) (n * y) :=
  SemiconjBy.mul_right (Int.commute_cast _ _) h
Integer Scalar Multiplication Preserves Semiconjugacy on the Right
Informal description
Let $a, x, y$ be elements of a semiring $\alpha$ such that $a$ semiconjugates $x$ to $y$ (i.e., $a \cdot x = y \cdot a$). Then for any integer $n$, the element $a$ semiconjugates $n \cdot x$ to $n \cdot y$, i.e., $a \cdot (n \cdot x) = (n \cdot y) \cdot a$.
SemiconjBy.intCast_mul_left theorem
(h : SemiconjBy a x y) (n : ℤ) : SemiconjBy (n * a) x y
Full source 
@[simp] lemma intCast_mul_left (h : SemiconjBy a x y) (n : ℤ) : SemiconjBy (n * a) x y :=
  SemiconjBy.mul_left (Int.cast_commute _ _) h
Integer Scalar Multiplication Preserves Semiconjugacy on the Left
Informal description
Let $a, x, y$ be elements of a semiring $\alpha$ such that $a$ semiconjugates $x$ to $y$ (i.e., $a \cdot x = y \cdot a$). Then for any integer $n$, the element $n \cdot a$ semiconjugates $x$ to $y$, i.e., $(n \cdot a) \cdot x = y \cdot (n \cdot a)$.
SemiconjBy.intCast_mul_intCast_mul theorem
(h : SemiconjBy a x y) (m n : ℤ) : SemiconjBy (m * a) (n * x) (n * y)
Full source 
@[simp] lemma intCast_mul_intCast_mul (h : SemiconjBy a x y) (m n : ℤ) :
    SemiconjBy (m * a) (n * x) (n * y) := (h.intCast_mul_left m).intCast_mul_right n
Integer Scalar Multiplication Preserves Semiconjugacy Bilaterally: $(m \cdot a) \cdot (n \cdot x) = (n \cdot y) \cdot (m \cdot a)$
Informal description
Let $a, x, y$ be elements of a semiring $\alpha$ such that $a$ semiconjugates $x$ to $y$ (i.e., $a \cdot x = y \cdot a$). Then for any integers $m$ and $n$, the element $m \cdot a$ semiconjugates $n \cdot x$ to $n \cdot y$, i.e., $(m \cdot a) \cdot (n \cdot x) = (n \cdot y) \cdot (m \cdot a)$.
Commute.intCast_left theorem
: Commute (n : α) a
Full source 
@[simp] lemma intCast_left : Commute (n : α) a := Int.cast_commute _ _
Integer Cast Commutes with Semiring Elements: $n \cdot a = a \cdot n$
Informal description
For any integer $n$ and any element $a$ in a semiring $\alpha$, the canonical image of $n$ in $\alpha$ commutes with $a$, i.e., $n \cdot a = a \cdot n$.
Commute.intCast_right theorem
: Commute a n
Full source 
@[simp] lemma intCast_right : Commute a n := Int.commute_cast _ _
Commutativity of Semiring Element with Integer Cast: $a \cdot n = n \cdot a$
Informal description
For any element $a$ in a semiring $\alpha$ and any integer $n$, the element $a$ commutes with the canonical image of $n$ in $\alpha$, i.e., $a \cdot n = n \cdot a$.
Commute.intCast_mul_right theorem
(h : Commute a b) (m : ℤ) : Commute a (m * b)
Full source 
@[simp] lemma intCast_mul_right (h : Commute a b) (m : ℤ) : Commute a (m * b) :=
  SemiconjBy.intCast_mul_right h m
Integer Scalar Multiplication Preserves Commutativity on the Right
Informal description
Let $a$ and $b$ be elements of a semiring $\alpha$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integer $m$, the elements $a$ and $m \cdot b$ commute, i.e., $a \cdot (m \cdot b) = (m \cdot b) \cdot a$.
Commute.intCast_mul_left theorem
(h : Commute a b) (m : ℤ) : Commute (m * a) b
Full source 
@[simp] lemma intCast_mul_left (h : Commute a b) (m : ℤ) : Commute (m  * a) b :=
  SemiconjBy.intCast_mul_left h m
Integer Scalar Multiplication Preserves Commutativity on the Left
Informal description
Let $a$ and $b$ be elements of a semiring $\alpha$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integer $m$, the elements $m \cdot a$ and $b$ commute, i.e., $(m \cdot a) \cdot b = b \cdot (m \cdot a)$.
Commute.intCast_mul_intCast_mul theorem
(h : Commute a b) (m n : ℤ) : Commute (m * a) (n * b)
Full source 
lemma intCast_mul_intCast_mul (h : Commute a b) (m n : ℤ) : Commute (m * a) (n * b) :=
  SemiconjBy.intCast_mul_intCast_mul h m n
Integer Scalar Multiplication Preserves Commutativity Bilaterally: $(m \cdot a) \cdot (n \cdot b) = (n \cdot b) \cdot (m \cdot a)$
Informal description
Let $a$ and $b$ be elements of a semiring $\alpha$ such that $a$ and $b$ commute (i.e., $a \cdot b = b \cdot a$). Then for any integers $m$ and $n$, the elements $m \cdot a$ and $n \cdot b$ commute, i.e., $(m \cdot a) \cdot (n \cdot b) = (n \cdot b) \cdot (m \cdot a)$.
Commute.self_intCast_mul theorem
: Commute a (n * a : α)
Full source 
lemma self_intCast_mul : Commute a (n * a : α) := (Commute.refl a).intCast_mul_right n
Commutativity of Element with its Integer Scalar Multiple
Informal description
For any integer $n$ and any element $a$ in a semiring $\alpha$, the element $a$ commutes with $n \cdot a$, i.e., $a \cdot (n \cdot a) = (n \cdot a) \cdot a$.
Commute.intCast_mul_self theorem
: Commute ((n : α) * a) a
Full source 
lemma intCast_mul_self : Commute ((n : α) * a) a := (Commute.refl a).intCast_mul_left n
Commutativity of Integer Scalar Multiplication with Element
Informal description
For any integer $n$ and any element $a$ in a semiring $\alpha$, the element $(n \cdot a)$ commutes with $a$, i.e., $(n \cdot a) \cdot a = a \cdot (n \cdot a)$.
Commute.self_intCast_mul_intCast_mul theorem
: Commute (m * a : α) (n * a : α)
Full source 
lemma self_intCast_mul_intCast_mul : Commute (m * a : α) (n * a : α) :=
  (Commute.refl a).intCast_mul_intCast_mul m n
Commutativity of Integer Scalar Multiples of the Same Element: $(m \cdot a) \cdot (n \cdot a) = (n \cdot a) \cdot (m \cdot a)$
Informal description
For any integers $m$ and $n$, and any element $a$ in a semiring $\alpha$, the elements $m \cdot a$ and $n \cdot a$ commute, i.e., $(m \cdot a) \cdot (n \cdot a) = (n \cdot a) \cdot (m \cdot a)$.
AddMonoidHom.ext_int theorem
[AddMonoid A] {f g : ℤ →+ A} (h1 : f 1 = g 1) : f = g
Full source 
/-- Two additive monoid homomorphisms `f`, `g` from `ℤ` to an additive monoid are equal
if `f 1 = g 1`. -/
@[ext high]
theorem ext_int [AddMonoid A] {f g : ℤℤ →+ A} (h1 : f 1 = g 1) : f = g :=
  have : f.comp (Int.ofNatHom : ℕℕ →+ ℤ) = g.comp (Int.ofNatHom : ℕℕ →+ ℤ) := ext_nat' _ _ h1
  have this' : ∀ n : ℕ, f n = g n := DFunLike.ext_iff.1 this
  ext fun n => match n with
  | (n : ℕ) => this' n
  | .negSucc n => eq_on_neg _ _ (this' <| n + 1)
Extensionality of Integer Additive Monoid Homomorphisms via Value at One
Informal description
Let $A$ be an additive monoid and let $f, g \colon \mathbb{Z} \to A$ be additive monoid homomorphisms. If $f(1) = g(1)$, then $f = g$.
map_intCast' theorem
[AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (h₁ : f 1 = 1) : ∀ n : ℤ, f n = n
Full source 
/-- This version is primed so that the `RingHomClass` versions aren't. -/
theorem map_intCast' [AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β]
    [AddMonoidHomClass F α β] (f : F) (h₁ : f 1 = 1) : ∀ n : ℤ, f n = n :=
  eq_intCast' ((f : α →+ β).comp <| Int.castAddHom _) (by simpa)
Additive Monoid Homomorphism Preserves Integer Casting
Informal description
Let $\alpha$ and $\beta$ be additive groups with one, and let $F$ be a type of functions from $\alpha$ to $\beta$ that form an additive monoid homomorphism class. For any $f \in F$ such that $f(1) = 1$, we have $f(n) = n$ for all integers $n \in \mathbb{Z}$.
Int.castAddHom_int theorem
: Int.castAddHom ℤ = AddMonoidHom.id ℤ
Full source 
@[simp]
theorem Int.castAddHom_int : Int.castAddHom ℤ = AddMonoidHom.id ℤ :=
  ((AddMonoidHom.id ℤ).eq_intCastAddHom rfl).symm
Canonical Integer Homomorphism is Identity on $\mathbb{Z}$
Informal description
The canonical additive monoid homomorphism from the integers $\mathbb{Z}$ to itself, $\text{Int.castAddHom} \colon \mathbb{Z} \to \mathbb{Z}$, is equal to the identity additive monoid homomorphism on $\mathbb{Z}$.
MonoidHom.ext_mint theorem
{f g : Multiplicative ℤ →* M} (h1 : f (ofAdd 1) = g (ofAdd 1)) : f = g
Full source 
@[ext]
theorem ext_mint {f g : MultiplicativeMultiplicative ℤ →* M} (h1 : f (ofAdd 1) = g (ofAdd 1)) : f = g :=
  MonoidHom.toAdditive''.injective <| AddMonoidHom.ext_int <| Additive.toMul.injective h1
Extensionality of Monoid Homomorphisms from Multiplicative Integers via Value at One
Informal description
Let $M$ be a monoid and let $f, g \colon \text{Multiplicative } \mathbb{Z} \to M$ be monoid homomorphisms. If $f(\text{ofAdd } 1) = g(\text{ofAdd } 1)$, then $f = g$.
MonoidHom.ext_int theorem
{f g : ℤ →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp Int.ofNatHom.toMonoidHom = g.comp Int.ofNatHom.toMonoidHom) : f = g
Full source 
/-- If two `MonoidHom`s agree on `-1` and the naturals then they are equal. -/
@[ext]
theorem ext_int {f g : ℤℤ →* M} (h_neg_one : f (-1) = g (-1))
    (h_nat : f.comp Int.ofNatHom.toMonoidHom = g.comp Int.ofNatHom.toMonoidHom) : f = g := by
  ext (x | x)
  · exact (DFunLike.congr_fun h_nat x :)
  · rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
    congr 1
    exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)
Equality of Monoid Homomorphisms from Integers via Agreement on $-1$ and Naturals
Informal description
Let $M$ be a monoid and let $f, g \colon \mathbb{Z} \to M$ be monoid homomorphisms. If $f(-1) = g(-1)$ and the compositions of $f$ and $g$ with the canonical homomorphism $\mathbb{N} \to \mathbb{Z}$ are equal, then $f = g$.
MonoidWithZeroHom.ext_int theorem
{f g : ℤ →*₀ M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom) : f = g
Full source 
/-- If two `MonoidWithZeroHom`s agree on `-1` and the naturals then they are equal. -/
@[ext]
theorem ext_int {f g : ℤℤ →*₀ M} (h_neg_one : f (-1) = g (-1))
    (h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom) :
    f = g :=
  toMonoidHom_injective <| MonoidHom.ext_int h_neg_one <|
    MonoidHom.ext (DFunLike.congr_fun h_nat :)
Uniqueness of Monoid with Zero Homomorphisms from Integers via Agreement on $-1$ and Naturals
Informal description
Let $M$ be a monoid with zero and let $f, g \colon \mathbb{Z} \to M$ be monoid with zero homomorphisms. If $f(-1) = g(-1)$ and the compositions of $f$ and $g$ with the canonical homomorphism $\mathbb{N} \to \mathbb{Z}$ are equal, then $f = g$.
ext_int' theorem
[MonoidWithZero α] [FunLike F ℤ α] [MonoidWithZeroHomClass F ℤ α] {f g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ n : ℕ, 0 < n → f n = g n) : f = g
Full source 
/-- If two `MonoidWithZeroHom`s agree on `-1` and the _positive_ naturals then they are equal. -/
theorem ext_int' [MonoidWithZero α] [FunLike F ℤ α] [MonoidWithZeroHomClass F ℤ α] {f g : F}
    (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  (DFunLike.ext _ _) fun n =>
    haveI :=
      DFunLike.congr_fun
        (@MonoidWithZeroHom.ext_int _ _ (f : ℤℤ →*₀ α) (g : ℤℤ →*₀ α) h_neg_one <|
          MonoidWithZeroHom.ext_nat (h_pos _))
        n
    this
Uniqueness of Monoid with Zero Homomorphisms from Integers via Agreement on $-1$ and Positive Naturals
Informal description
Let $\alpha$ be a monoid with zero and let $F$ be a type of functions from $\mathbb{Z}$ to $\alpha$ that preserves the monoid with zero structure. For any two functions $f, g \in F$, if $f(-1) = g(-1)$ and $f(n) = g(n)$ for all positive natural numbers $n$, then $f = g$.
zmultiplesHom definition
: β ≃ (ℤ →+ β)
Full source 
/-- Additive homomorphisms from `ℤ` are defined by the image of `1`. -/
def zmultiplesHom : β ≃ (ℤ →+ β) where
  toFun x :=
  { toFun := fun n => n • x
    map_zero' := zero_zsmul x
    map_add' := fun _ _ => add_zsmul _ _ _ }
  invFun f := f 1
  left_inv := one_zsmul
  right_inv f := AddMonoidHom.ext_int <| one_zsmul (f 1)
Equivalence between group elements and integer homomorphisms
Informal description
The equivalence `zmultiplesHom` establishes a bijection between elements of an additive group `β` and additive group homomorphisms from the integers `ℤ` to `β`. Specifically: 1. The forward map sends an element `x ∈ β` to the homomorphism `n ↦ n • x` (where `•` denotes integer scalar multiplication) 2. The inverse map evaluates a homomorphism `f : ℤ →+ β` at `1`, returning `f(1) ∈ β` This equivalence satisfies: 1. `zmultiplesHom⁻¹ ∘ zmultiplesHom = id` (left inverse property) 2. `zmultiplesHom ∘ zmultiplesHom⁻¹ = id` (right inverse property)
zpowersHom definition
: α ≃ (Multiplicative ℤ →* α)
Full source 
/-- Monoid homomorphisms from `Multiplicative ℤ` are defined by the image
of `Multiplicative.ofAdd 1`. -/
@[to_additive existing]
def zpowersHom : α ≃ (Multiplicative ℤ →* α) :=
  ofMul.trans <| (zmultiplesHom _).trans <| AddMonoidHom.toMultiplicative''
Equivalence between group elements and integer power homomorphisms
Informal description
The equivalence `zpowersHom` establishes a bijection between elements of a multiplicative group `α` and group homomorphisms from the integers (in multiplicative form) to `α`. Specifically: 1. The forward map sends an element `x ∈ α` to the homomorphism `n ↦ x^n` (where exponentiation uses integer powers) 2. The inverse map evaluates a homomorphism `f : Multiplicative ℤ →* α` at the generator `ofAdd 1`, returning `f(ofAdd 1) ∈ α` This equivalence satisfies: 1. `zpowersHom⁻¹ ∘ zpowersHom = id` (left inverse property) 2. `zpowersHom ∘ zpowersHom⁻¹ = id` (right inverse property)
zmultiplesHom_apply theorem
(x : β) (n : ℤ) : zmultiplesHom β x n = n • x
Full source 
lemma zmultiplesHom_apply (x : β) (n : ℤ) : zmultiplesHom β x n = n • x := rfl
Evaluation of Integer Multiples Homomorphism
Informal description
For any element $x$ in an additive group $\beta$ and any integer $n \in \mathbb{Z}$, the evaluation of the homomorphism `zmultiplesHom β x` at $n$ equals the integer scalar multiplication $n \cdot x$.
zmultiplesHom_symm_apply theorem
(f : ℤ →+ β) : (zmultiplesHom β).symm f = f 1
Full source 
lemma zmultiplesHom_symm_apply (f : ℤℤ →+ β) : (zmultiplesHom β).symm f = f 1 := rfl
Inverse of `zmultiplesHom` Evaluates Homomorphism at 1
Informal description
For any additive group homomorphism $f \colon \mathbb{Z} \to \beta$, the inverse of the `zmultiplesHom` equivalence evaluated at $f$ is equal to $f(1)$. In other words, $(zmultiplesHom_\beta)^{-1}(f) = f(1)$.
zpowersHom_apply theorem
(x : α) (n : Multiplicative ℤ) : zpowersHom α x n = x ^ n.toAdd
Full source 
@[to_additive existing (attr := simp)]
lemma zpowersHom_apply (x : α) (n : Multiplicative ℤ) : zpowersHom α x n = x ^ n.toAdd := rfl
Evaluation of Integer Power Homomorphism: $(\text{zpowersHom}_\alpha\,x)\,n = x^n$
Informal description
For any element $x$ in a multiplicative group $\alpha$ and any integer $n$ (represented multiplicatively as `Multiplicative ℤ`), the evaluation of the homomorphism `zpowersHom α x` at $n$ equals $x$ raised to the power of the additive interpretation of $n$, i.e., $x^{n}$.
zpowersHom_symm_apply theorem
(f : Multiplicative ℤ →* α) : (zpowersHom α).symm f = f (ofAdd 1)
Full source 
@[to_additive existing (attr := simp)]
lemma zpowersHom_symm_apply (f : MultiplicativeMultiplicative ℤ →* α) :
    (zpowersHom α).symm f = f (ofAdd 1) := rfl
Inverse of `zpowersHom` Evaluates Homomorphism at 1
Informal description
For any group homomorphism $f \colon \mathbb{Z} \to \alpha$ (where $\mathbb{Z}$ is considered multiplicatively), the inverse of the `zpowersHom` equivalence evaluated at $f$ is equal to $f(1)$. In other words, $(zpowersHom_\alpha)^{-1}(f) = f(1)$.
MonoidHom.apply_mint theorem
(f : Multiplicative ℤ →* α) (n : Multiplicative ℤ) : f n = f (ofAdd 1) ^ n.toAdd
Full source 
lemma MonoidHom.apply_mint (f : MultiplicativeMultiplicative ℤ →* α) (n : Multiplicative ℤ) :
    f n = f (ofAdd 1) ^ n.toAdd := by
  rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
Evaluation of Monoid Homomorphism on Integers via Powers of $f(1)$
Informal description
For any monoid homomorphism $f \colon \mathbb{Z} \to \alpha$ (where $\mathbb{Z}$ is considered multiplicatively) and any integer $n$ (represented multiplicatively as `Multiplicative ℤ`), the evaluation of $f$ at $n$ equals $f(1)$ raised to the power of $n$, i.e., $f(n) = f(1)^n$.
AddMonoidHom.apply_int theorem
(f : ℤ →+ β) (n : ℤ) : f n = n • f 1
Full source 
lemma AddMonoidHom.apply_int (f : ℤℤ →+ β) (n : ℤ) : f n = n • f 1 := by
  rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
Evaluation of Integer Additive Homomorphism via Scalar Multiplication
Informal description
For any additive group homomorphism $f \colon \mathbb{Z} \to \beta$ and any integer $n \in \mathbb{Z}$, the evaluation of $f$ at $n$ equals the integer scalar multiplication of $n$ with $f(1)$, i.e., $f(n) = n \cdot f(1)$.
zmultiplesAddHom definition
: β ≃+ (ℤ →+ β)
Full source 
/-- If `α` is commutative, `zmultiplesHom` is an additive equivalence. -/
def zmultiplesAddHom : β ≃+ (ℤ →+ β) :=
  { zmultiplesHom β with map_add' := fun a b => AddMonoidHom.ext fun n => by simp [zsmul_add] }
Additive equivalence between group elements and integer homomorphisms preserving addition
Informal description
The additive equivalence `zmultiplesAddHom` is a bijection between elements of an additive commutative group `β` and additive group homomorphisms from the integers `ℤ` to `β`. It extends `zmultiplesHom` by additionally preserving the additive structure, meaning that for any `a, b ∈ β`, the map satisfies `zmultiplesAddHom (a + b) = zmultiplesAddHom a + zmultiplesAddHom b` as additive group homomorphisms. More precisely: 1. The forward map sends an element `x ∈ β` to the homomorphism `n ↦ n • x` (where `•` denotes integer scalar multiplication) 2. The inverse map evaluates a homomorphism `f : ℤ →+ β` at `1`, returning `f(1) ∈ β` 3. The equivalence preserves addition: `zmultiplesAddHom (a + b) = zmultiplesAddHom a + zmultiplesAddHom b` for all `a, b ∈ β`
zpowersMulHom definition
: α ≃* (Multiplicative ℤ →* α)
Full source 
/-- If `α` is commutative, `zpowersHom` is a multiplicative equivalence. -/
def zpowersMulHom : α ≃* (Multiplicative ℤ →* α) :=
  { zpowersHom α with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_zpow] }
Multiplicative equivalence between group elements and integer power homomorphisms
Informal description
The multiplicative equivalence `zpowersMulHom` establishes a bijection between elements of a commutative group `α` and group homomorphisms from the integers (in multiplicative form) to `α`. Specifically: 1. The forward map sends an element `x ∈ α` to the homomorphism `n ↦ x^n` (where exponentiation uses integer powers) 2. The inverse map evaluates a homomorphism `f : Multiplicative ℤ →* α` at the generator `ofAdd 1`, returning `f(ofAdd 1) ∈ α` This equivalence preserves multiplication, meaning that for any `x, y ∈ α`, the map satisfies `zpowersMulHom (x * y) = zpowersMulHom x * zpowersMulHom y` as group homomorphisms.
zpowersMulHom_apply theorem
(x : α) (n : Multiplicative ℤ) : zpowersMulHom α x n = x ^ n.toAdd
Full source 
@[simp]
lemma zpowersMulHom_apply (x : α) (n : Multiplicative ℤ) : zpowersMulHom α x n = x ^ n.toAdd := rfl
Evaluation of Multiplicative Equivalence at Integer Power: $\text{zpowersMulHom}_\alpha(x)(n) = x^n$
Informal description
For any element $x$ in a commutative group $\alpha$ and any integer $n$ (represented multiplicatively as `Multiplicative ℤ`), the multiplicative equivalence `zpowersMulHom` evaluated at $x$ and $n$ equals $x$ raised to the power of $n$, i.e., $\text{zpowersMulHom}_\alpha(x)(n) = x^{n}$.
zpowersMulHom_symm_apply theorem
(f : Multiplicative ℤ →* α) : (zpowersMulHom α).symm f = f (ofAdd 1)
Full source 
@[simp]
lemma zpowersMulHom_symm_apply (f : MultiplicativeMultiplicative ℤ →* α) :
    (zpowersMulHom α).symm f = f (ofAdd 1) := rfl
Inverse of `zpowersMulHom` Evaluates at Generator: $(zpowersMulHom_\alpha)^{-1}(f) = f(1)$
Informal description
For any group homomorphism $f \colon \mathbb{Z} \to \alpha$ (where $\mathbb{Z}$ is considered multiplicatively), the inverse of the multiplicative equivalence `zpowersMulHom` evaluated at $f$ is equal to $f(1)$, where $1$ is the integer $1$ in multiplicative form.
zmultiplesAddHom_apply theorem
(x : β) (n : ℤ) : zmultiplesAddHom β x n = n • x
Full source 
@[simp] lemma zmultiplesAddHom_apply (x : β) (n : ℤ) : zmultiplesAddHom β x n = n • x := rfl
Evaluation of Additive Equivalence at Integer Scalar Multiplication
Informal description
For any element $x$ in an additive commutative group $\beta$ and any integer $n \in \mathbb{Z}$, the additive equivalence `zmultiplesAddHom` evaluated at $x$ and $n$ equals the integer scalar multiplication of $n$ and $x$, i.e., $(\text{zmultiplesAddHom}_{\beta}\,x)(n) = n \cdot x$.
zmultiplesAddHom_symm_apply theorem
(f : ℤ →+ β) : (zmultiplesAddHom β).symm f = f 1
Full source 
@[simp] lemma zmultiplesAddHom_symm_apply (f : ℤℤ →+ β) : (zmultiplesAddHom β).symm f = f 1 := rfl
Inverse of `zmultiplesAddHom` evaluates at 1: $(zmultiplesAddHom_\beta)^{-1}(f) = f(1)$
Informal description
For any additive group homomorphism $f \colon \mathbb{Z} \to \beta$, the inverse of the additive equivalence `zmultiplesAddHom` evaluated at $f$ is equal to $f(1)$.
map_intCast theorem
[FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f n = n
Full source 
@[simp]
theorem map_intCast [FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f n = n :=
  eq_intCast ((f : α →+* β).comp (Int.castRingHom α)) n
Ring homomorphisms preserve integer scalars: $f(n) = n$
Informal description
For any ring homomorphism $f$ from a ring $\alpha$ to a ring $\beta$ (i.e., $f \in \text{RingHomClass}\,F\,\alpha\,\beta$), and for any integer $n \in \mathbb{Z}$, the image of $n$ under $f$ is equal to $n$ itself, i.e., $f(n) = n$.
RingHom.Int.subsingleton_ringHom instance
{R : Type*} [NonAssocSemiring R] : Subsingleton (ℤ →+* R)
Full source 
instance Int.subsingleton_ringHom {R : Type*} [NonAssocSemiring R] : Subsingleton (ℤℤ →+* R) :=
  ⟨RingHom.ext_int⟩
Uniqueness of Ring Homomorphisms from Integers to a Non-Associative Semiring
Informal description
For any non-associative semiring $R$, there is at most one ring homomorphism from the integers $\mathbb{Z}$ to $R$.
Int.castRingHom_int theorem
: Int.castRingHom ℤ = RingHom.id ℤ
Full source 
@[simp]
theorem Int.castRingHom_int : Int.castRingHom ℤ = RingHom.id ℤ :=
  (RingHom.id ℤ).eq_intCast'.symm
Identity Property of Integer Cast Ring Homomorphism: $\text{castRingHom}_{\mathbb{Z}} = \text{id}_{\mathbb{Z}}$
Informal description
The canonical ring homomorphism from the integers $\mathbb{Z}$ to itself is equal to the identity ring homomorphism on $\mathbb{Z}$.