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 #

Coercion ℕ → ℤ as a RingHom.

Equations
@[simp]
theorem Int.cast_ite {α : Type u_3} [IntCast α] (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
@[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_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
@[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} [Ring α] (m n : ) (h : m n) :
m n
@[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
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)
@[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
theorem Commute.intCast_mul_right {α : Type u_3} [Ring α] {a b : α} (h : Commute a b) (m : ) :
Commute a (m * b)
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)
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.ext_int_iff {A : Type u_5} [AddMonoid A] {f g : →+ A} :
f = g f 1 = g 1
theorem AddMonoidHom.eq_intCastAddHom {A : Type u_5} [AddGroupWithOne A] (f : →+ A) (h1 : f 1 = 1) :
theorem AddEquiv.ext_int {A : Type u_5} [AddMonoid A] {f g : ≃+ A} (h1 : f 1 = g 1) :
f = g

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

theorem AddEquiv.ext_int_iff {A : Type u_5} [AddMonoid A] {f g : ≃+ A} :
f = g f 1 = g 1
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.

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 MonoidHom.ext_int_iff {M : Type u_5} [Monoid M] {f g : →* M} :
f = g f (-1) = g (-1) f.comp Int.ofNatHom = g.comp Int.ofNatHom
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 < nf 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 α] :

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

Equations
@[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 ) :
@[simp]
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
def zpowersMulHom (α : Type u_3) [CommGroup α] :

If α is commutative, zpowersHom is a multiplicative equivalence.

Equations
@[simp]
theorem zpowersMulHom_apply {α : Type u_3} [CommGroup α] (x : α) (n : Multiplicative ) :
@[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 : →+ β) :
@[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 : →+* α) :
theorem RingHom.ext_int {R : Type u_5} [NonAssocSemiring R] (f g : →+* R) :
f = g