# 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.

Coercion ℕ → ℤ as a RingHom.

Equations
Instances For
@[simp]
theorem Int.cast_ite {α : Type u_3} [] (P : Prop) [] (m : ) (n : ) :
(if P then m else n) = if P then m else n
def Int.castAddHom (α : Type u_5) [] :

coe : ℤ → α as an AddMonoidHom.

Equations
• = { toFun := Int.cast, map_zero' := , map_add' := }
Instances For
@[simp]
theorem Int.coe_castAddHom {α : Type u_3} [] :
() = fun (x : ) => x
def Int.castRingHom (α : Type u_3) [] :

coe : ℤ → α as a RingHom.

Equations
• = { toFun := Int.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Int.coe_castRingHom {α : Type u_3} [] :
() = fun (x : ) => x
theorem Int.cast_commute {α : Type u_3} [] (n : ) (a : α) :
Commute (n) a
theorem Int.cast_comm {α : Type u_3} [] (n : ) (x : α) :
n * x = x * n
theorem Int.commute_cast {α : Type u_3} [] (a : α) (n : ) :
Commute a n
@[simp]
theorem zsmul_eq_mul {α : Type u_3} [Ring α] (a : α) (n : ) :
n a = n * a
theorem zsmul_eq_mul' {α : Type u_3} [Ring α] (a : α) (n : ) :
n a = a * n
theorem Int.cast_mono {α : Type u_3} [] :
Monotone fun (x : ) => x
@[simp]
theorem Int.cast_nonneg {α : Type u_3} [] [] {n : } :
0 n 0 n
@[simp]
theorem Int.cast_le {α : Type u_3} [] [] {m : } {n : } :
m n m n
theorem Int.cast_strictMono {α : Type u_3} [] [] :
StrictMono fun (x : ) => x
@[simp]
theorem Int.cast_lt {α : Type u_3} [] [] {m : } {n : } :
m < n m < n
@[simp]
theorem Int.cast_nonpos {α : Type u_3} [] [] {n : } :
n 0 n 0
@[simp]
theorem Int.cast_pos {α : Type u_3} [] [] {n : } :
0 < n 0 < n
@[simp]
theorem Int.cast_lt_zero {α : Type u_3} [] [] {n : } :
n < 0 n < 0
@[simp]
theorem Int.cast_min {α : Type u_3} {a : } {b : } :
(min a b) = min a b
@[simp]
theorem Int.cast_max {α : Type u_3} {a : } {b : } :
(max a b) = max a b
@[simp]
theorem Int.cast_abs {α : Type u_3} {a : } :
|a| = |a|
theorem Int.cast_one_le_of_pos {α : Type u_3} {a : } (h : 0 < a) :
1 a
theorem Int.cast_le_neg_one_of_neg {α : Type u_3} {a : } (h : a < 0) :
a -1
theorem Int.cast_le_neg_one_or_one_le_cast_of_ne_zero (α : Type u_3) {n : } (hn : n 0) :
n -1 1 n
theorem Int.nneg_mul_add_sq_of_abs_le_one {α : Type u_3} (n : ) {x : α} (hx : |x| 1) :
0 n * x + n * n
theorem Int.cast_natAbs {α : Type u_3} (n : ) :
n.natAbs = |n|
theorem Int.coe_int_dvd {α : Type u_3} [] (m : ) (n : ) (h : m n) :
m n
@[simp]
theorem SemiconjBy.cast_int_mul_right {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
SemiconjBy a (n * x) (n * y)
@[simp]
theorem SemiconjBy.cast_int_mul_left {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
SemiconjBy (n * a) x y
@[simp]
theorem SemiconjBy.cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (m : ) (n : ) :
SemiconjBy (m * a) (n * x) (n * y)
@[simp]
theorem Commute.cast_int_left {α : Type u_3} [] {a : α} {n : } :
Commute (n) a
@[simp]
theorem Commute.cast_int_right {α : Type u_3} [] {a : α} {n : } :
Commute a n
@[simp]
theorem Commute.cast_int_mul_right {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
Commute a (m * b)
@[simp]
theorem Commute.cast_int_mul_left {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) :
Commute (m * a) b
theorem Commute.cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] {a : α} {b : α} (h : Commute a b) (m : ) (n : ) :
Commute (m * a) (n * b)
theorem Commute.self_cast_int_mul {α : Type u_3} [Ring α] (a : α) (n : ) :
Commute a (n * a)
theorem Commute.cast_int_mul_self {α : Type u_3} [Ring α] (a : α) (n : ) :
Commute (n * a) a
theorem Commute.self_cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] (a : α) (m : ) (n : ) :
Commute (m * a) (n * a)
theorem AddMonoidHom.ext_int {A : Type u_5} [] {f : →+ A} {g : →+ A} (h1 : f 1 = g 1) :
f = g

Two additive monoid homomorphisms f, g from ℤ to an additive monoid are equal if f 1 = g 1.

theorem AddMonoidHom.eq_intCastAddHom {A : Type u_5} [] (f : →+ A) (h1 : f 1 = 1) :
theorem eq_intCast' {F : Type u_1} {α : Type u_3} [] [FunLike F α] [] (f : F) (h₁ : f 1 = 1) (n : ) :
f n = n
@[simp]
theorem zsmul_one {α : Type u_3} [] (n : ) :
n 1 = n
@[simp]
theorem MonoidHom.ext_mint {M : Type u_5} [] {f : } {g : } (h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
f = g
theorem MonoidHom.ext_int {M : Type u_5} [] {f : →* M} {g : →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp = g.comp ) :
f = g

If two MonoidHoms agree on -1 and the naturals then they are equal.

theorem MonoidWithZeroHom.ext_int {M : Type u_5} [] {f : →*₀ M} {g : →*₀ M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom) :
f = g

If two MonoidWithZeroHoms agree on -1 and the naturals then they are equal.

theorem ext_int' {F : Type u_1} {α : Type u_3} [] [FunLike F α] [] {f : F} {g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ (n : ), 0 < nf n = g n) :
f = g

If two MonoidWithZeroHoms agree on -1 and the positive naturals then they are equal.

def zmultiplesHom (α : Type u_3) [] :
α ( →+ α)

Additive homomorphisms from ℤ are defined by the image of 1.

Equations
• = { toFun := fun (x : α) => { toFun := fun (n : ) => n x, map_zero' := , map_add' := }, invFun := fun (f : →+ α) => f 1, left_inv := , right_inv := }
Instances For
def zpowersHom (α : Type u_3) [] :
α ()

Monoid homomorphisms from Multiplicative ℤ are defined by the image of Multiplicative.ofAdd 1.

Equations
Instances For
@[simp]
theorem zmultiplesHom_apply (α : Type u_3) [] (x : α) (n : ) :
(() x) n = n x
@[simp]
theorem zmultiplesHom_symm_apply (α : Type u_3) [] (f : →+ α) :
().symm f = f 1
@[simp]
theorem zpowersHom_apply (α : Type u_3) [] (x : α) (n : ) :
(() x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem zpowersHom_symm_apply (α : Type u_3) [] (f : ) :
().symm f = f (Multiplicative.ofAdd 1)
theorem MonoidHom.apply_mint (α : Type u_3) [] (f : ) (n : ) :
theorem AddMonoidHom.apply_int (α : Type u_3) [] (f : →+ α) (n : ) :
f n = n f 1
def zmultiplesAddHom (α : Type u_3) [] :
α ≃+ ( →+ α)

If α is commutative, zmultiplesHom is an additive equivalence.

Equations
• = let __src := ; { toEquiv := __src, map_add' := }
Instances For
def zpowersMulHom (α : Type u_3) [] :
α ≃* ()

If α is commutative, zpowersHom is a multiplicative equivalence.

Equations
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem zpowersMulHom_apply {α : Type u_3} [] (x : α) (n : ) :
(() x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem zpowersMulHom_symm_apply {α : Type u_3} [] (f : ) :
().symm f = f (Multiplicative.ofAdd 1)
@[simp]
theorem zmultiplesAddHom_apply {α : Type u_3} [] (x : α) (n : ) :
(() x) n = n x
@[simp]
theorem zmultiplesAddHom_symm_apply {α : Type u_3} [] (f : →+ α) :
().symm f = f 1
@[simp]
theorem eq_intCast {F : Type u_1} {α : Type u_3} [] [FunLike F α] [] (f : F) (n : ) :
f n = n
@[simp]
theorem map_intCast {F : Type u_1} {α : Type u_3} {β : Type u_4} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (n : ) :
f n = n
theorem RingHom.eq_intCast' {α : Type u_3} [] (f : →+* α) :
theorem RingHom.ext_int {R : Type u_5} [] (f : →+* R) (g : →+* R) :
f = g
Equations
• =
@[simp]
instance Pi.instIntCast {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] :
IntCast ((i : ι) → π i)
Equations
• Pi.instIntCast = { intCast := fun (n : ) (x : ι) => n }
theorem Pi.intCast_apply {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) (i : ι) :
n i = n
@[simp]
theorem Pi.intCast_def {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) :
n = fun (x : ι) => n
@[deprecated Pi.intCast_apply]
theorem Pi.int_apply {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) (i : ι) :
n i = n

Alias of Pi.intCast_apply.

@[deprecated Pi.intCast_def]
theorem Pi.coe_int {ι : Type u_2} {π : ιType u_5} [(i : ι) → IntCast (π i)] (n : ) :
n = fun (x : ι) => n

Alias of Pi.intCast_def.

theorem Sum.elim_intCast_intCast {α : Type u_5} {β : Type u_6} {γ : Type u_7} [] (n : ) :
Sum.elim n n = n

### Order dual #

instance instIntCastOrderDual {α : Type u_3} [h : ] :
Equations
• instIntCastOrderDual = h
instance instAddGroupWithOneOrderDual {α : Type u_3} [h : ] :
Equations
instance instAddCommGroupWithOneOrderDual {α : Type u_3} [h : ] :
Equations
@[simp]
theorem toDual_intCast {α : Type u_3} [] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem ofDual_intCast {α : Type u_3} [] (n : ) :
OrderDual.ofDual n = n

### Lexicographic order #

instance instIntCastLex {α : Type u_3} [h : ] :
Equations
• instIntCastLex = h
instance instAddGroupWithOneLex {α : Type u_3} [h : ] :
Equations