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 ℤ

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_mul {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (n : ℤ) :

↑(m * n) = ↑m * ↑n

@[simp]

theorem Int.cast_ite {α : Type u_1} [inst : AddGroupWithOne α] (P : Prop) [inst : Decidable P] (m : ℤ) (n : ℤ) :

↑(if P then m else n) = if P then ↑m else ↑n

def Int.castAddHom (α : Type u_1) [inst : 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_1} [inst : AddGroupWithOne α] :

↑(Int.castAddHom α) = fun x => ↑x

def Int.castRingHom (α : Type u_1) [inst : 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_1} [inst : NonAssocRing α] :

↑(Int.castRingHom α) = fun x => ↑x

theorem Int.cast_commute {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (x : α) :

Commute (↑m) x

theorem Int.cast_comm {α : Type u_1} [inst : NonAssocRing α] (m : ℤ) (x : α) :

↑m * x = x * ↑m

theorem Int.commute_cast {α : Type u_1} [inst : NonAssocRing α] (x : α) (m : ℤ) :

Commute x ↑m

theorem Int.cast_mono {α : Type u_1} [inst : OrderedRing α] :

Monotone fun x => ↑x

@[simp]

theorem Int.cast_nonneg {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : ℤ} :

0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem Int.cast_le {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {m : ℤ} {n : ℤ} :

↑m ≤ ↑n ↔ m ≤ n

theorem Int.cast_strictMono {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] :

StrictMono fun x => ↑x

@[simp]

theorem Int.cast_lt {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {m : ℤ} {n : ℤ} :

↑m < ↑n ↔ m < n

@[simp]

theorem Int.cast_nonpos {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : ℤ} :

↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem Int.cast_pos {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : ℤ} :

0 < ↑n ↔ 0 < n

@[simp]

theorem Int.cast_lt_zero {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {n : ℤ} :

↑n < 0 ↔ n < 0

@[simp]

theorem Int.cast_min {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ} {b : ℤ} :

↑(min a b) = min ↑a ↑b

@[simp]

theorem Int.cast_max {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ} {b : ℤ} :

↑(max a b) = max ↑a ↑b

@[simp]

theorem Int.cast_abs {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ} :

↑(abs a) = abs ↑a

theorem Int.cast_one_le_of_pos {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ} (h : 0 < a) :

1 ≤ ↑a

theorem Int.cast_le_neg_one_of_neg {α : Type u_1} [inst : LinearOrderedRing α] {a : ℤ} (h : a < 0) :

↑a ≤ -1

theorem Int.cast_le_neg_one_or_one_le_cast_of_ne_zero (α : Type u_1) [inst : LinearOrderedRing α] {n : ℤ} (hn : n ≠ 0) :

↑n ≤ -1 ∨ 1 ≤ ↑n

theorem Int.nneg_mul_add_sq_of_abs_le_one {α : Type u_1} [inst : LinearOrderedRing α] (n : ℤ) {x : α} (hx : abs x ≤ 1) :

0 ≤ ↑n * x + ↑n * ↑n

theorem Int.cast_natAbs {α : Type u_1} [inst : LinearOrderedRing α] (n : ℤ) :

↑(Int.natAbs n) = ↑(abs n)

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

↑m ∣ ↑n

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

f = Int.castAddHom A

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

↑f n = ↑n

@[simp]

theorem Int.castAddHom_int :

Int.castAddHom ℤ = AddMonoidHom.id ℤ

theorem MonoidHom.ext_mint {M : Type u_1} [inst : 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_1} [inst : 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_1} [inst : 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_2} {α : Type u_1} [inst : MonoidWithZero α] [inst : 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.

@[simp]

theorem eq_intCast {F : Type u_1} {α : Type u_2} [inst : NonAssocRing α] [inst : RingHomClass F ℤ α] (f : F) (n : ℤ) :

↑f n = ↑n

@[simp]

theorem map_intCast {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst : NonAssocRing β] [inst : RingHomClass F α β] (f : F) (n : ℤ) :

↑f ↑n = ↑n

theorem RingHom.eq_intCast' {α : Type u_1} [inst : NonAssocRing α] (f : ℤ →+* α) :

f = Int.castRingHom α

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

f = g

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

Subsingleton (ℤ →+* R)

Equations

@RingHom.Int.subsingleton_ringHom = @RingHom.Int.subsingleton_ringHom.proof_1

@[simp]

theorem Int.castRingHom_int :

Int.castRingHom ℤ = RingHom.id ℤ

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

IntCast ((i : ι) → π i)

Equations

Pi.intCast = { intCast := fun n x => ↑n }

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

↑n i = ↑n

@[simp]

theorem Pi.coe_int {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → IntCast (π i)] (n : ℤ) :

↑n = fun x => ↑n

theorem Sum.elim_intCast_intCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : IntCast γ] (n : ℤ) :

Sum.elim ↑n ↑n = ↑n

Order dual #

instance instIntCastOrderDual {α : Type u_1} [h : IntCast α] :

IntCast αᵒᵈ

Equations

instIntCastOrderDual = h

instance instAddGroupWithOneOrderDual {α : Type u_1} [h : AddGroupWithOne α] :

AddGroupWithOne αᵒᵈ

Equations

instAddGroupWithOneOrderDual = h

instance instAddCommGroupWithOneOrderDual {α : Type u_1} [h : AddCommGroupWithOne α] :

AddCommGroupWithOne αᵒᵈ

Equations

instAddCommGroupWithOneOrderDual = h

@[simp]

theorem toDual_intCast {α : Type u_1} [inst : IntCast α] (n : ℤ) :

↑OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_intCast {α : Type u_1} [inst : IntCast α] (n : ℤ) :

↑(↑OrderDual.ofDual n) = ↑n

Lexicographic order #

instance instIntCastLex {α : Type u_1} [h : IntCast α] :

IntCast (Lex α)

Equations

instIntCastLex = h

instance instAddGroupWithOneLex {α : Type u_1} [h : AddGroupWithOne α] :

AddGroupWithOne (Lex α)

Equations

instAddGroupWithOneLex = h

instance instAddCommGroupWithOneLex {α : Type u_1} [h : AddCommGroupWithOne α] :

AddCommGroupWithOne (Lex α)

Equations

instAddCommGroupWithOneLex = h

@[simp]

theorem toLex_intCast {α : Type u_1} [inst : IntCast α] (n : ℤ) :

↑toLex ↑n = ↑n

@[simp]

theorem ofLex_intCast {α : Type u_1} [inst : IntCast α] (n : ℤ) :

↑(↑ofLex n) = ↑n