data.nat.cast.basic - mathlib3 docs

source

def nat.cast_add_monoid_hom (α : Type u_1) [add_monoid_with_one α] :

ℕ →+ α

coe : ℕ → α as an add_monoid_hom.

Equations

nat.cast_add_monoid_hom α = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

theorem nat.coe_cast_add_monoid_hom {α : Type u_1} [add_monoid_with_one α] :

⇑(nat.cast_add_monoid_hom α) = coe

source

@[simp, norm_cast]

theorem nat.cast_mul {α : Type u_1} [non_assoc_semiring α] (m n : ℕ) :

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

source

def nat.cast_ring_hom (α : Type u_1) [non_assoc_semiring α] :

ℕ →+* α

coe : ℕ → α as a ring_hom

Equations

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

source

@[simp]

theorem nat.coe_cast_ring_hom {α : Type u_1} [non_assoc_semiring α] :

⇑(nat.cast_ring_hom α) = coe

source

theorem nat.cast_commute {α : Type u_1} [non_assoc_semiring α] (n : ℕ) (x : α) :

commute ↑n x

source

theorem nat.cast_comm {α : Type u_1} [non_assoc_semiring α] (n : ℕ) (x : α) :

↑n * x = x * ↑n

source

theorem nat.commute_cast {α : Type u_1} [non_assoc_semiring α] (x : α) (n : ℕ) :

commute x ↑n

source

theorem nat.mono_cast {α : Type u_1} [ordered_semiring α] :

monotone coe

source

@[simp]

theorem nat.cast_nonneg {α : Type u_1} [ordered_semiring α] (n : ℕ) :

0 ≤ ↑n

source

theorem nat.cast_add_one_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] (n : ℕ) :

0 < ↑n + 1

source

@[simp]

theorem nat.cast_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :

0 < ↑n ↔ 0 < n

source

theorem nat.strict_mono_cast {α : Type u_1} [ordered_semiring α] [char_zero α] :

strict_mono coe

source

def nat.cast_order_embedding {α : Type u_1} [ordered_semiring α] [char_zero α] :

ℕ ↪o α

coe : ℕ → α as an order_embedding

Equations

nat.cast_order_embedding = order_embedding.of_strict_mono coe nat.strict_mono_cast

source

@[simp]

theorem nat.cast_order_embedding_apply {α : Type u_1} [ordered_semiring α] [char_zero α] :

⇑nat.cast_order_embedding = coe

source

@[simp, norm_cast]

theorem nat.cast_le {α : Type u_1} [ordered_semiring α] [char_zero α] {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

source

@[simp, norm_cast]

theorem nat.cast_lt {α : Type u_1} [ordered_semiring α] [char_zero α] {m n : ℕ} :

↑m < ↑n ↔ m < n

source

@[simp, norm_cast]

theorem nat.one_lt_cast {α : Type u_1} [ordered_semiring α] [char_zero α] {n : ℕ} :

1 < ↑n ↔ 1 < n

source

@[simp, norm_cast]

theorem nat.one_le_cast {α : Type u_1} [ordered_semiring α] [char_zero α] {n : ℕ} :

1 ≤ ↑n ↔ 1 ≤ n

source

@[simp, norm_cast]

theorem nat.cast_lt_one {α : Type u_1} [ordered_semiring α] [char_zero α] {n : ℕ} :

↑n < 1 ↔ n = 0

source

@[simp, norm_cast]

theorem nat.cast_le_one {α : Type u_1} [ordered_semiring α] [char_zero α] {n : ℕ} :

↑n ≤ 1 ↔ n ≤ 1

source

@[simp, norm_cast]

theorem nat.cast_tsub {α : Type u_1} [canonically_ordered_comm_semiring α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] (m n : ℕ) :

↑(m - n) = ↑m - ↑n

A version of nat.cast_sub that works for ℝ≥0 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

source

@[simp, norm_cast]

theorem nat.cast_min {α : Type u_1} [linear_ordered_semiring α] {a b : ℕ} :

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

source

@[simp, norm_cast]

theorem nat.cast_max {α : Type u_1} [linear_ordered_semiring α] {a b : ℕ} :

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

source

@[simp, norm_cast]

theorem nat.abs_cast {α : Type u_1} [linear_ordered_ring α] (a : ℕ) :

|↑a| = ↑a

source

theorem nat.coe_nat_dvd {α : Type u_1} [semiring α] {m n : ℕ} (h : m ∣ n) :

↑m ∣ ↑n

source

theorem has_dvd.dvd.nat_cast {α : Type u_1} [semiring α] {m n : ℕ} (h : m ∣ n) :

↑m ∣ ↑n

Alias of nat.coe_nat_dvd.

source

theorem ext_nat' {A : Type u_3} {F : Type u_5} [add_monoid A] [add_monoid_hom_class F ℕ A] (f g : F) (h : ⇑f 1 = ⇑g 1) :

f = g

source

@[ext]

theorem add_monoid_hom.ext_nat {A : Type u_3} [add_monoid A] {f g : ℕ →+ A} (h : ⇑f 1 = ⇑g 1) :

f = g

source

theorem eq_nat_cast' {A : Type u_3} {F : Type u_5} [add_monoid_with_one A] [add_monoid_hom_class F ℕ A] (f : F) (h1 : ⇑f 1 = 1) (n : ℕ) :

⇑f n = ↑n

source

theorem map_nat_cast' {B : Type u_4} {F : Type u_5} [add_monoid_with_one B] {A : Type u_1} [add_monoid_with_one A] [add_monoid_hom_class F A B] (f : F) (h : ⇑f 1 = 1) (n : ℕ) :

⇑f ↑n = ↑n

source

theorem ext_nat'' {A : Type u_3} {F : Type u_4} [mul_zero_one_class A] [monoid_with_zero_hom_class F ℕ A] (f g : F) (h_pos : ∀ {n : ℕ}, 0 < n → ⇑f n = ⇑g n) :

f = g

If two monoid_with_zero_homs agree on the positive naturals they are equal.

source

@[ext]

theorem monoid_with_zero_hom.ext_nat {A : Type u_3} [mul_zero_one_class A] {f g : ℕ →*₀ A} :

(∀ {n : ℕ}, 0 < n → ⇑f n = ⇑g n) → f = g

source

@[simp]

theorem eq_nat_cast {R : Type u_3} {F : Type u_5} [non_assoc_semiring R] [ring_hom_class F ℕ R] (f : F) (n : ℕ) :

⇑f n = ↑n

source

@[simp]

theorem map_nat_cast {R : Type u_3} {S : Type u_4} {F : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [ring_hom_class F R S] (f : F) (n : ℕ) :

⇑f ↑n = ↑n

source

theorem ext_nat {R : Type u_3} {F : Type u_5} [non_assoc_semiring R] [ring_hom_class F ℕ R] (f g : F) :

f = g

source

theorem ne_zero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] {n : ℕ} [h : ne_zero ↑n] [ring_hom_class F R S] {f : F} (hf : function.injective ⇑f) :

ne_zero ↑n

source

theorem ne_zero.nat_of_ne_zero {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {F : Type u_3} [ring_hom_class F R S] (f : F) {n : ℕ} [hn : ne_zero ↑n] :

ne_zero ↑n

source