mathlib3 documentation

data.int.cast.lemmas

Cast of integers (additional theorems) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

cast_add_hom: cast bundled as an add_monoid_hom.
cast_ring_hom: cast bundled as a ring_hom.

def int.of_nat_hom :

Coercion ℕ → ℤ as a ring_hom.

Equations

int.of_nat_hom = {to_fun := coe coe_to_lift, map_one' := int.of_nat_hom._proof_1, map_mul' := int.of_nat_mul, map_zero' := int.of_nat_hom._proof_2, map_add' := int.of_nat_add}

@[simp]

theorem int.coe_nat_pos {n : ℕ} :

0 < ↑n ↔ 0 < n

theorem int.coe_nat_succ_pos (n : ℕ) :

0 < ↑(n.succ)

theorem int.to_nat_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) :

a.to_nat < b ↔ a < ↑b

theorem int.nat_mod_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) :

a.nat_mod ↑b < b

@[simp, norm_cast]

theorem int.cast_mul {α : Type u_3} [non_assoc_ring α] (m n : ℤ) :

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

@[simp, norm_cast]

theorem int.cast_ite {α : Type u_3} [add_group_with_one α] (P : Prop) [decidable P] (m n : ℤ) :

↑(ite P m n) = ite P ↑m ↑n

def int.cast_add_hom (α : Type u_1) [add_group_with_one α] :

coe : ℤ → α as an add_monoid_hom.

Equations

int.cast_add_hom α = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

@[simp]

theorem int.coe_cast_add_hom {α : Type u_3} [add_group_with_one α] :

⇑(int.cast_add_hom α) = coe

def int.cast_ring_hom (α : Type u_1) [non_assoc_ring α] :

coe : ℤ → α as a ring_hom.

Equations

int.cast_ring_hom α = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem int.coe_cast_ring_hom {α : Type u_3} [non_assoc_ring α] :

⇑(int.cast_ring_hom α) = coe

theorem int.cast_commute {α : Type u_3} [non_assoc_ring α] (m : ℤ) (x : α) :

theorem int.cast_comm {α : Type u_3} [non_assoc_ring α] (m : ℤ) (x : α) :

↑m * x = x * ↑m

theorem int.commute_cast {α : Type u_3} [non_assoc_ring α] (x : α) (m : ℤ) :

theorem int.cast_mono {α : Type u_3} [ordered_ring α] :

@[simp]

theorem int.cast_nonneg {α : Type u_3} [ordered_ring α] [nontrivial α] {n : ℤ} :

0 ≤ ↑n ↔ 0 ≤ n

@[simp, norm_cast]

theorem int.cast_le {α : Type u_3} [ordered_ring α] [nontrivial α] {m n : ℤ} :

↑m ≤ ↑n ↔ m ≤ n

theorem int.cast_strict_mono {α : Type u_3} [ordered_ring α] [nontrivial α] :

strict_mono coe

@[simp, norm_cast]

theorem int.cast_lt {α : Type u_3} [ordered_ring α] [nontrivial α] {m n : ℤ} :

↑m < ↑n ↔ m < n

@[simp]

theorem int.cast_nonpos {α : Type u_3} [ordered_ring α] [nontrivial α] {n : ℤ} :

↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem int.cast_pos {α : Type u_3} [ordered_ring α] [nontrivial α] {n : ℤ} :

0 < ↑n ↔ 0 < n

@[simp]

theorem int.cast_lt_zero {α : Type u_3} [ordered_ring α] [nontrivial α] {n : ℤ} :

↑n < 0 ↔ n < 0

@[simp, norm_cast]

theorem int.cast_min {α : Type u_3} [linear_ordered_ring α] {a b : ℤ} :

↑(linear_order.min a b) = linear_order.min ↑a ↑b

@[simp, norm_cast]

theorem int.cast_max {α : Type u_3} [linear_ordered_ring α] {a b : ℤ} :

↑(linear_order.max a b) = linear_order.max ↑a ↑b

@[simp, norm_cast]

theorem int.cast_abs {α : Type u_3} [linear_ordered_ring α] {a : ℤ} :

↑|a| = |↑a|

theorem int.cast_one_le_of_pos {α : Type u_3} [linear_ordered_ring α] {a : ℤ} (h : 0 < a) :

theorem int.cast_le_neg_one_of_neg {α : Type u_3} [linear_ordered_ring α] {a : ℤ} (h : a < 0) :

theorem int.cast_le_neg_one_or_one_le_cast_of_ne_zero (α : Type u_3) [linear_ordered_ring α] {n : ℤ} (hn : n ≠ 0) :

↑n ≤ -1 ∨ 1 ≤ ↑n

theorem int.nneg_mul_add_sq_of_abs_le_one {α : Type u_3} [linear_ordered_ring α] (n : ℤ) {x : α} (hx : |x| ≤ 1) :

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

theorem int.cast_nat_abs {α : Type u_3} [linear_ordered_ring α] (n : ℤ) :

↑(n.nat_abs) = |↑n|

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

@[ext]

theorem add_monoid_hom.ext_int {A : Type u_5} [add_monoid 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 add_monoid_hom.eq_int_cast_hom {A : Type u_5} [add_group_with_one A] (f : ℤ →+ A) (h1 : ⇑f 1 = 1) :

f = int.cast_add_hom A

theorem eq_int_cast' {F : Type u_1} {α : Type u_3} [add_group_with_one α] [add_monoid_hom_class F ℤ α] (f : F) (h₁ : ⇑f 1 = 1) (n : ℤ) :

@[simp]

theorem int.cast_add_hom_int :

int.cast_add_hom ℤ = add_monoid_hom.id ℤ

@[ext]

theorem monoid_hom.ext_mint {M : Type u_5} [monoid M] {f g : multiplicative ℤ →* M} (h1 : ⇑f (⇑multiplicative.of_add 1) = ⇑g (⇑multiplicative.of_add 1)) :

f = g

@[ext]

theorem monoid_hom.ext_int {M : Type u_5} [monoid M] {f g : ℤ →* M} (h_neg_one : ⇑f (-1) = ⇑g (-1)) (h_nat : f.comp int.of_nat_hom.to_monoid_hom = g.comp int.of_nat_hom.to_monoid_hom) :

f = g

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

@[ext]

theorem monoid_with_zero_hom.ext_int {M : Type u_5} [monoid_with_zero M] {f g : ℤ →*₀ M} (h_neg_one : ⇑f (-1) = ⇑g (-1)) (h_nat : f.comp int.of_nat_hom.to_monoid_with_zero_hom = g.comp int.of_nat_hom.to_monoid_with_zero_hom) :

f = g

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

theorem ext_int' {F : Type u_1} {α : Type u_3} [monoid_with_zero α] [monoid_with_zero_hom_class F ℤ α] {f g : F} (h_neg_one : ⇑f (-1) = ⇑g (-1)) (h_pos : ∀ (n : ℕ), 0 < n → ⇑f ↑n = ⇑g ↑n) :

f = g

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

@[simp]

theorem eq_int_cast {F : Type u_1} {α : Type u_3} [non_assoc_ring α] [ring_hom_class F ℤ α] (f : F) (n : ℤ) :

@[simp]

theorem map_int_cast {F : Type u_1} {α : Type u_3} {β : Type u_4} [non_assoc_ring α] [non_assoc_ring β] [ring_hom_class F α β] (f : F) (n : ℤ) :

⇑f ↑n = ↑n

theorem ring_hom.eq_int_cast' {α : Type u_3} [non_assoc_ring α] (f : ℤ →+* α) :

f = int.cast_ring_hom α

theorem ring_hom.ext_int {R : Type u_1} [non_assoc_semiring R] (f g : ℤ →+* R) :

f = g

@[protected, instance]

def ring_hom.int.subsingleton_ring_hom {R : Type u_1} [non_assoc_semiring R] :

subsingleton (ℤ →+* R)

@[simp, norm_cast]

theorem int.cast_id (n : ℤ) :

↑n = n

@[simp]

theorem int.cast_ring_hom_int :

int.cast_ring_hom ℤ = ring_hom.id ℤ

@[protected, instance]

def pi.has_int_cast {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] :

has_int_cast (Π (i : ι), π i)

Equations

pi.has_int_cast = {int_cast := λ (ᾰ : ℤ), id (λ (i : ι), has_int_cast.int_cast ᾰ)}

theorem pi.int_apply {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] (n : ℤ) (i : ι) :

@[simp]

theorem pi.coe_int {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] (n : ℤ) :

↑n = λ (_x : ι), ↑n

theorem sum.elim_int_cast_int_cast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_int_cast γ] (n : ℤ) :

sum.elim ↑n ↑n = ↑n

@[protected, instance]

def pi.add_group_with_one {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), add_group_with_one (π i)] :

add_group_with_one (Π (i : ι), π i)

Equations

pi.add_group_with_one = {int_cast := λ (ᾰ : ℤ), id (λ (i : ι), add_group_with_one.int_cast ᾰ), add := λ (ᾰ ᾰ_1 : Π (i : ι), π i), id (λ (i : ι), add_group_with_one.add (ᾰ i) (ᾰ_1 i)), add_assoc := _, zero := id (λ (i : ι), add_group_with_one.zero), zero_add := _, add_zero := _, nsmul := λ (ᾰ : ℕ) (ᾰ_1 : Π (i : ι), π i), id (λ (i : ι), add_group_with_one.nsmul ᾰ (ᾰ_1 i)), nsmul_zero' := _, nsmul_succ' := _, neg := λ (ᾰ : Π (i : ι), π i), id (λ (i : ι), add_group_with_one.neg (ᾰ i)), sub := λ (ᾰ ᾰ_1 : Π (i : ι), π i), id (λ (i : ι), add_group_with_one.sub (ᾰ i) (ᾰ_1 i)), sub_eq_add_neg := _, zsmul := λ (ᾰ : ℤ) (ᾰ_1 : Π (i : ι), π i), id (λ (i : ι), add_group_with_one.zsmul ᾰ (ᾰ_1 i)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (ᾰ : ℕ), id (λ (i : ι), add_group_with_one.nat_cast ᾰ), one := id (λ (i : ι), add_group_with_one.one), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

Order dual #

@[protected, instance]

def order_dual.has_int_cast {α : Type u_3} [h : has_int_cast α] :

has_int_cast αᵒᵈ

Equations

order_dual.has_int_cast = h

@[protected, instance]

def order_dual.add_group_with_one {α : Type u_3} [h : add_group_with_one α] :

add_group_with_one αᵒᵈ

Equations

order_dual.add_group_with_one = h

@[protected, instance]

def order_dual.add_comm_group_with_one {α : Type u_3} [h : add_comm_group_with_one α] :

add_comm_group_with_one αᵒᵈ

Equations

order_dual.add_comm_group_with_one = h

@[simp]

theorem to_dual_int_cast {α : Type u_3} [has_int_cast α] (n : ℤ) :

⇑order_dual.to_dual ↑n = ↑n

@[simp]

theorem of_dual_int_cast {α : Type u_3} [has_int_cast α] (n : ℤ) :

↑(⇑order_dual.of_dual n) = ↑n

Lexicographic order #

@[protected, instance]

def lex.has_int_cast {α : Type u_3} [h : has_int_cast α] :

has_int_cast (lex α)

Equations

lex.has_int_cast = h

@[protected, instance]

def lex.add_group_with_one {α : Type u_3} [h : add_group_with_one α] :

add_group_with_one (lex α)

Equations

lex.add_group_with_one = h

@[protected, instance]

def lex.add_comm_group_with_one {α : Type u_3} [h : add_comm_group_with_one α] :

add_comm_group_with_one (lex α)

Equations

lex.add_comm_group_with_one = h

@[simp]

theorem to_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ℤ) :

⇑to_lex ↑n = ↑n

@[simp]

theorem of_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ℤ) :

↑(⇑of_lex n) = ↑n