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.

def Int.ofNatHom : ℕ →+* ℤ

Coercion ℕ → ℤ as a RingHom.

Equations

• Int.ofNatHom = Nat.castRingHom ℤ

theorem Int.coe_nat_pos {n : ℕ} : 0 < ↑n ↔ 0 < n

theorem Int.coe_nat_succ_pos (n : ℕ) : 0 < ↑(Nat.succ n)

theorem Int.toNat_lt' {a : ℤ} {b : ℕ} (hb : b ≠ 0) : Int.toNat a < b ↔ a < ↑b

theorem Int.natMod_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) : Int.natMod a ↑b < b

@[simp]

theorem Int.cast_ite {α : Type u_3} [AddGroupWithOne α] (P : Prop) [Decidable P] (m : ℤ) (n : ℤ) : ↑(if P then m else n) = if P then ↑m else ↑n

def Int.castAddHom (α : Type u_5) [AddGroupWithOne α] : ℤ →+ α

coe : ℤ → α as an AddMonoidHom.

Equations

• Int.castAddHom α = { toZeroHom := { toFun := Int.cast, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (m n : ℤ), ↑(m + n) = ↑m + ↑n) }

@[simp]

theorem Int.coe_castAddHom {α : Type u_3} [AddGroupWithOne α] : ⇑(Int.castAddHom α) = fun (x : ℤ) => ↑x

def Int.castRingHom (α : Type u_3) [NonAssocRing α] : ℤ →+* α

coe : ℤ → α as a RingHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Int.coe_castRingHom {α : Type u_3} [NonAssocRing α] : ⇑(Int.castRingHom α) = fun (x : ℤ) => ↑x

theorem Int.cast_commute {α : Type u_3} [NonAssocRing α] (n : ℤ) (a : α) : Commute (↑n) a

theorem Int.cast_comm {α : Type u_3} [NonAssocRing α] (n : ℤ) (x : α) : ↑n * x = x * ↑n

theorem Int.commute_cast {α : Type u_3} [NonAssocRing α] (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} [OrderedRing α] : Monotone fun (x : ℤ) => ↑x

@[simp]

theorem Int.cast_nonneg {α : Type u_3} [OrderedRing α] [Nontrivial α] {n : ℤ} : 0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem Int.cast_le {α : Type u_3} [OrderedRing α] [Nontrivial α] {m : ℤ} {n : ℤ} : ↑m ≤ ↑n ↔ m ≤ n

theorem Int.cast_strictMono {α : Type u_3} [OrderedRing α] [Nontrivial α] : StrictMono fun (x : ℤ) => ↑x

@[simp]

theorem Int.cast_lt {α : Type u_3} [OrderedRing α] [Nontrivial α] {m : ℤ} {n : ℤ} : ↑m < ↑n ↔ m < n

@[simp]

theorem Int.cast_nonpos {α : Type u_3} [OrderedRing α] [Nontrivial α] {n : ℤ} : ↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem Int.cast_pos {α : Type u_3} [OrderedRing α] [Nontrivial α] {n : ℤ} : 0 < ↑n ↔ 0 < n

@[simp]

theorem Int.cast_lt_zero {α : Type u_3} [OrderedRing α] [Nontrivial α] {n : ℤ} : ↑n < 0 ↔ n < 0

@[simp]

theorem Int.cast_min {α : Type u_3} [LinearOrderedRing α] {a : ℤ} {b : ℤ} : ↑(min a b) = min ↑a ↑b

@[simp]

theorem Int.cast_max {α : Type u_3} [LinearOrderedRing α] {a : ℤ} {b : ℤ} : ↑(max a b) = max ↑a ↑b

@[simp]

theorem Int.cast_abs {α : Type u_3} [LinearOrderedRing α] {a : ℤ} : ↑|a| = |↑a|

theorem Int.cast_one_le_of_pos {α : Type u_3} [LinearOrderedRing α] {a : ℤ} (h : 0 < a) : 1 ≤ ↑a

theorem Int.cast_le_neg_one_of_neg {α : Type u_3} [LinearOrderedRing α] {a : ℤ} (h : a < 0) : ↑a ≤ -1

theorem Int.cast_le_neg_one_or_one_le_cast_of_ne_zero (α : Type u_3) [LinearOrderedRing α] {n : ℤ} (hn : n ≠ 0) : ↑n ≤ -1 ∨ 1 ≤ ↑n

theorem Int.nneg_mul_add_sq_of_abs_le_one {α : Type u_3} [LinearOrderedRing α] (n : ℤ) {x : α} (hx : |x| ≤ 1) : 0 ≤ ↑n * x + ↑n * ↑n

theorem Int.cast_natAbs {α : Type u_3} [LinearOrderedRing α] (n : ℤ) : ↑(Int.natAbs n) = ↑|n|

theorem Int.coe_int_dvd {α : Type u_3} [CommRing α] (m : ℤ) (n : ℤ) (h : m ∣ n) : ↑m ∣ ↑n

theorem Int.coe_nat_pow (m : ℕ) (n : ℕ) : ↑(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} [NonAssocRing α] {a : α} {n : ℤ} : Commute (↑n) a

@[simp]

theorem Commute.cast_int_right {α : Type u_3} [NonAssocRing α] {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} [AddMonoid A] {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_int_castAddHom {A : Type u_5} [AddGroupWithOne A] (f : ℤ →+ A) (h1 : f 1 = 1) : f = Int.castAddHom A

theorem eq_intCast' {F : Type u_1} {α : Type u_3} [AddGroupWithOne α] [FunLike F ℤ α] [AddMonoidHomClass F ℤ α] (f : F) (h₁ : f 1 = 1) (n : ℤ) : f n = ↑n

@[simp]

theorem zsmul_one {α : Type u_3} [AddGroupWithOne α] (n : ℤ) : n • 1 = ↑n

@[simp]

theorem Int.castAddHom_int : Int.castAddHom ℤ = AddMonoidHom.id ℤ

theorem MonoidHom.ext_mint {M : Type u_5} [Monoid M] {f : Multiplicative ℤ →* M} {g : Multiplicative ℤ →* M} (h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

theorem MonoidHom.ext_int {M : Type u_5} [Monoid M] {f : ℤ →* M} {g : ℤ →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : MonoidHom.comp f ↑Int.ofNatHom = MonoidHom.comp g ↑Int.ofNatHom) : f = g

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

theorem MonoidWithZeroHom.ext_int {M : Type u_5} [MonoidWithZero M] {f : ℤ →*₀ M} {g : ℤ →*₀ M} (h_neg_one : f (-1) = g (-1)) (h_nat : MonoidWithZeroHom.comp f (RingHom.toMonoidWithZeroHom Int.ofNatHom) = MonoidWithZeroHom.comp g (RingHom.toMonoidWithZeroHom Int.ofNatHom)) : 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} [MonoidWithZero α] [FunLike F ℤ α] [MonoidWithZeroHomClass F ℤ α] {f : F} {g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n) : f = g

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

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

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

Equations

• One or more equations did not get rendered due to their size.

def zpowersHom (α : Type u_3) [Group α] : α ≃ (Multiplicative ℤ →* α)

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

Equations

• zpowersHom α = Additive.ofMul.trans ((zmultiplesHom (Additive α)).trans AddMonoidHom.toMultiplicative'')

@[simp]

theorem zmultiplesHom_apply (α : Type u_3) [AddGroup α] (x : α) (n : ℤ) : ((zmultiplesHom α) x) n = n • x

@[simp]

theorem zmultiplesHom_symm_apply (α : Type u_3) [AddGroup α] (f : ℤ →+ α) : (zmultiplesHom α).symm f = f 1

@[simp]

theorem zpowersHom_apply (α : Type u_3) [Group α] (x : α) (n : Multiplicative ℤ) : ((zpowersHom α) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem zpowersHom_symm_apply (α : Type u_3) [Group α] (f : Multiplicative ℤ →* α) : (zpowersHom α).symm f = f (Multiplicative.ofAdd 1)

theorem MonoidHom.apply_mint (α : Type u_3) [Group α] (f : Multiplicative ℤ →* α) (n : Multiplicative ℤ) : f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n

theorem AddMonoidHom.apply_int (α : Type u_3) [AddGroup α] (f : ℤ →+ α) (n : ℤ) : f n = n • f 1

def zmultiplesAddHom (α : Type u_3) [AddCommGroup α] : α ≃+ (ℤ →+ α)

If α is commutative, zmultiplesHom is an additive equivalence.

Equations

• One or more equations did not get rendered due to their size.

def zpowersMulHom (α : Type u_3) [CommGroup α] : α ≃* (Multiplicative ℤ →* α)

If α is commutative, zpowersHom is a multiplicative equivalence.

Equations

• zpowersMulHom α = let src := zpowersHom α; { toEquiv := src, map_mul' := (_ : ∀ (a b : α), (zpowersHom α).toFun (a * b) = (zpowersHom α).toFun a * (zpowersHom α).toFun b) }

@[simp]

theorem zpowersMulHom_apply {α : Type u_3} [CommGroup α] (x : α) (n : Multiplicative ℤ) : ((zpowersMulHom α) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem zpowersMulHom_symm_apply {α : Type u_3} [CommGroup α] (f : Multiplicative ℤ →* α) : (MulEquiv.symm (zpowersMulHom α)) f = f (Multiplicative.ofAdd 1)

@[simp]

theorem zmultiplesAddHom_apply {α : Type u_3} [AddCommGroup α] (x : α) (n : ℤ) : ((zmultiplesAddHom α) x) n = n • x

@[simp]

theorem zmultiplesAddHom_symm_apply {α : Type u_3} [AddCommGroup α] (f : ℤ →+ α) : (AddEquiv.symm (zmultiplesAddHom α)) f = f 1

@[simp]

theorem eq_intCast {F : Type u_1} {α : Type u_3} [NonAssocRing α] [FunLike F ℤ α] [RingHomClass F ℤ α] (f : F) (n : ℤ) : f n = ↑n

@[simp]

theorem map_intCast {F : Type u_1} {α : Type u_3} {β : Type u_4} [NonAssocRing α] [NonAssocRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f ↑n = ↑n

theorem RingHom.eq_intCast' {α : Type u_3} [NonAssocRing α] (f : ℤ →+* α) : f = Int.castRingHom α

theorem RingHom.ext_int {R : Type u_5} [NonAssocSemiring R] (f : ℤ →+* R) (g : ℤ →+* R) : f = g

instance RingHom.Int.subsingleton_ringHom {R : Type u_5} [NonAssocSemiring R] : Subsingleton (ℤ →+* R)

Equations

• (_ : Subsingleton (ℤ →+* R)) = (_ : Subsingleton (ℤ →+* R))

@[simp]

theorem Int.castRingHom_int : Int.castRingHom ℤ = RingHom.id ℤ

instance Pi.intCast {ι : Type u_2} {π : ι → Type u_5} [(i : ι) → IntCast (π i)] : IntCast ((i : ι) → π i)

Equations

• Pi.intCast = { intCast := fun (n : ℤ) (x : ι) => ↑n }

theorem Pi.int_apply {ι : Type u_2} {π : ι → Type u_5} [(i : ι) → IntCast (π i)] (n : ℤ) (i : ι) : ↑n i = ↑n

@[simp]

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

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

Order dual

instance instIntCastOrderDual {α : Type u_3} [h : IntCast α] : IntCast αᵒᵈ

Equations

• instIntCastOrderDual = h

instance instAddGroupWithOneOrderDual {α : Type u_3} [h : AddGroupWithOne α] : AddGroupWithOne αᵒᵈ

Equations

• instAddGroupWithOneOrderDual = h

instance instAddCommGroupWithOneOrderDual {α : Type u_3} [h : AddCommGroupWithOne α] : AddCommGroupWithOne αᵒᵈ

Equations

• instAddCommGroupWithOneOrderDual = h

@[simp]

theorem toDual_intCast {α : Type u_3} [IntCast α] (n : ℤ) : OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_intCast {α : Type u_3} [IntCast α] (n : ℤ) : OrderDual.ofDual ↑n = ↑n

Lexicographic order

instance instIntCastLex {α : Type u_3} [h : IntCast α] : IntCast (Lex α)

Equations

• instIntCastLex = h

instance instAddGroupWithOneLex {α : Type u_3} [h : AddGroupWithOne α] : AddGroupWithOne (Lex α)

Equations

• instAddGroupWithOneLex = h

instance instAddCommGroupWithOneLex {α : Type u_3} [h : AddCommGroupWithOne α] : AddCommGroupWithOne (Lex α)

Equations

• instAddCommGroupWithOneLex = h

@[simp]

theorem toLex_intCast {α : Type u_3} [IntCast α] (n : ℤ) : toLex ↑n = ↑n

@[simp]

theorem ofLex_intCast {α : Type u_3} [IntCast α] (n : ℤ) : ofLex ↑n = ↑n