Documentation

Mathlib.Data.Int.Cast.Lemmas

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 ℤ

@[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 α = { toFun := Int.cast, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Int.coe_castAddHom {α : Type u_3} [AddGroupWithOne α] :

⇑(castAddHom α) = fun (x : ℤ) => ↑x

theorem Even.intCast {α : Type u_3} [AddGroupWithOne α] {n : ℤ} (h : Even n) :

Even ↑n

@[simp]

theorem Int.cast_eq_zero {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : ℤ} :

↑n = 0 ↔ n = 0

@[simp]

theorem Int.cast_inj {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m n : ℤ} :

↑m = ↑n ↔ m = n

theorem Int.cast_injective {α : Type u_3} [AddGroupWithOne α] [CharZero α] :

Function.Injective Int.cast

theorem Int.cast_ne_zero {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : ℤ} :

↑n ≠ 0 ↔ n ≠ 0

@[simp]

theorem Int.cast_eq_one {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : ℤ} :

↑n = 1 ↔ n = 1

theorem Int.cast_ne_one {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : ℤ} :

↑n ≠ 1 ↔ n ≠ 1

def Int.castRingHom (α : Type u_3) [NonAssocRing α] :

coe : ℤ → α as a RingHom.

Equations

Int.castRingHom α = { toFun := Int.cast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Int.coe_castRingHom {α : Type u_3} [NonAssocRing α] :

⇑(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} [NonAssocRing α] (a : α) (n : ℤ) :

n • a = ↑n * a

theorem zsmul_eq_mul' {α : Type u_3} [NonAssocRing α] (a : α) (n : ℤ) :

n • a = a * ↑n

theorem Odd.intCast {α : Type u_3} [Ring α] {n : ℤ} (hn : Odd n) :

Odd ↑n

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

↑m ∣ ↑n

@[deprecated Int.cast_dvd_cast (since := "2024-05-25")]

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

↑m ∣ ↑n

Alias of Int.cast_dvd_cast.

@[simp]

theorem SemiconjBy.intCast_mul_right {α : Type u_3} [Ring α] {a x y : α} (h : SemiconjBy a x y) (n : ℤ) :

SemiconjBy a (↑n * x) (↑n * y)

@[simp]

theorem SemiconjBy.intCast_mul_left {α : Type u_3} [Ring α] {a x y : α} (h : SemiconjBy a x y) (n : ℤ) :

SemiconjBy (↑n * a) x y

@[simp]

theorem SemiconjBy.intCast_mul_intCast_mul {α : Type u_3} [Ring α] {a x y : α} (h : SemiconjBy a x y) (m n : ℤ) :

SemiconjBy (↑m * a) (↑n * x) (↑n * y)

@[deprecated SemiconjBy.intCast_mul_right (since := "2024-05-27")]

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)

Alias of SemiconjBy.intCast_mul_right.

@[deprecated SemiconjBy.intCast_mul_left (since := "2024-05-27")]

theorem SemiconjBy.cast_int_mul_left {α : Type u_3} [Ring α] {a x y : α} (h : SemiconjBy a x y) (n : ℤ) :

SemiconjBy (↑n * a) x y

Alias of SemiconjBy.intCast_mul_left.

@[deprecated SemiconjBy.intCast_mul_intCast_mul (since := "2024-05-27")]

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)

Alias of SemiconjBy.intCast_mul_intCast_mul.

@[simp]

theorem Commute.intCast_left {α : Type u_3} [NonAssocRing α] {a : α} {n : ℤ} :

Commute (↑n) a

@[simp]

theorem Commute.intCast_right {α : Type u_3} [NonAssocRing α] {a : α} {n : ℤ} :

Commute a ↑n

@[deprecated Commute.intCast_right (since := "2024-05-27")]

theorem Commute.cast_int_right {α : Type u_3} [NonAssocRing α] {a : α} {n : ℤ} :

Commute a ↑n

Alias of Commute.intCast_right.

@[deprecated Commute.intCast_left (since := "2024-05-27")]

theorem Commute.cast_int_left {α : Type u_3} [NonAssocRing α] {a : α} {n : ℤ} :

Commute (↑n) a

Alias of Commute.intCast_left.

@[simp]

theorem Commute.intCast_mul_right {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ℤ) :

Commute a (↑m * b)

@[simp]

theorem Commute.intCast_mul_left {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ℤ) :

Commute (↑m * a) b

theorem Commute.intCast_mul_intCast_mul {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m n : ℤ) :

Commute (↑m * a) (↑n * b)

theorem Commute.self_intCast_mul {α : Type u_3} [Ring α] (a : α) (n : ℤ) :

Commute a (↑n * a)

theorem Commute.intCast_mul_self {α : Type u_3} [Ring α] (a : α) (n : ℤ) :

Commute (↑n * a) a

theorem Commute.self_intCast_mul_intCast_mul {α : Type u_3} [Ring α] (a : α) (m n : ℤ) :

Commute (↑m * a) (↑n * a)

@[deprecated Commute.intCast_mul_right (since := "2024-05-27")]

theorem Commute.cast_int_mul_right {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ℤ) :

Commute a (↑m * b)

Alias of Commute.intCast_mul_right.

@[deprecated Commute.intCast_mul_left (since := "2024-05-27")]

theorem Commute.cast_int_mul_left {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ℤ) :

Commute (↑m * a) b

Alias of Commute.intCast_mul_left.

@[deprecated Commute.intCast_mul_intCast_mul (since := "2024-05-27")]

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)

Alias of Commute.intCast_mul_intCast_mul.

@[deprecated Commute.self_intCast_mul (since := "2024-05-27")]

theorem Commute.self_cast_int_mul {α : Type u_3} [Ring α] (a : α) (n : ℤ) :

Commute a (↑n * a)

Alias of Commute.self_intCast_mul.

@[deprecated Commute.intCast_mul_self (since := "2024-05-27")]

theorem Commute.cast_int_mul_self {α : Type u_3} [Ring α] (a : α) (n : ℤ) :

Commute (↑n * a) a

Alias of Commute.intCast_mul_self.

@[deprecated Commute.self_intCast_mul_intCast_mul (since := "2024-05-27")]

theorem Commute.self_cast_int_mul_cast_int_mul {α : Type u_3} [Ring α] (a : α) (m n : ℤ) :

Commute (↑m * a) (↑n * a)

Alias of Commute.self_intCast_mul_intCast_mul.

theorem AddMonoidHom.ext_int {A : Type u_5} [AddMonoid A] {f 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} [AddGroupWithOne A] (f : ℤ →+ A) (h1 : f 1 = 1) :

f = Int.castAddHom A

@[deprecated AddMonoidHom.eq_intCastAddHom (since := "2024-04-17")]

theorem AddMonoidHom.eq_int_castAddHom {A : Type u_5} [AddGroupWithOne A] (f : ℤ →+ A) (h1 : f 1 = 1) :

f = Int.castAddHom A

Alias of AddMonoidHom.eq_intCastAddHom.

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

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

f ↑n = ↑n

This version is primed so that the RingHomClass versions aren't.

@[simp]

theorem Int.castAddHom_int :

castAddHom ℤ = AddMonoidHom.id ℤ

theorem MonoidHom.ext_mint {M : Type u_5} [Monoid M] {f 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 g : ℤ →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : f.comp ↑Int.ofNatHom = g.comp ↑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 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} [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

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

def zmultiplesHom (β : Type u_4) [AddGroup β] :

β ≃ (ℤ →+ β)

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

Equations

zmultiplesHom β = { toFun := fun (x : β) => { toFun := fun (n : ℤ) => n • x, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun (f : ℤ →+ β) => f 1, left_inv := ⋯, right_inv := ⋯ }

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_4) [AddGroup β] (x : β) (n : ℤ) :

((zmultiplesHom β) x) n = n • x

@[simp]

theorem zmultiplesHom_symm_apply (β : Type u_4) [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_4) [AddGroup β] (f : ℤ →+ β) (n : ℤ) :

f n = n • f 1

def zmultiplesAddHom (β : Type u_4) [AddCommGroup β] :

β ≃+ (ℤ →+ β)

If α is commutative, zmultiplesHom is an additive equivalence.

Equations

zmultiplesAddHom β = { toEquiv := zmultiplesHom β, map_add' := ⋯ }

def zpowersMulHom (α : Type u_3) [CommGroup α] :

α ≃* (Multiplicative ℤ →* α)

If α is commutative, zpowersHom is a multiplicative equivalence.

Equations

zpowersMulHom α = { toEquiv := zpowersHom α, map_mul' := ⋯ }

@[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 ℤ →* α) :

(zpowersMulHom α).symm f = f (Multiplicative.ofAdd 1)

@[simp]

theorem zmultiplesAddHom_apply (β : Type u_4) [AddCommGroup β] (x : β) (n : ℤ) :

((zmultiplesAddHom β) x) n = n • x

@[simp]

theorem zmultiplesAddHom_symm_apply (β : Type u_4) [AddCommGroup β] (f : ℤ →+ β) :

(zmultiplesAddHom β).symm 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 g : ℤ →+* R) :

f = g

instance RingHom.Int.subsingleton_ringHom {R : Type u_5} [NonAssocSemiring R] :

Subsingleton (ℤ →+* R)

@[simp]

theorem Int.castRingHom_int :

castRingHom ℤ = RingHom.id ℤ