mathlib documentation

data.nat.cast

Cast of naturals #

This file defines the canonical homomorphism from the natural numbers into a type α with 0, 1 and + (typically an add_monoid with one).

Main declarations #

Implementation note #

Setting up the coercions priorities is tricky. See Note [coercion into rings].

source
@[protected]
def nat.cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
ℕ → α

Canonical homomorphism from ℕ to a type α with 0, 1 and +.

Equations
source
@[protected]
def nat.bin_cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
α

Computationally friendlier cast than nat.cast, using binary representation.

Equations
source
@[protected, instance]
def nat.cast_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
has_coe_t ℕ α
Equations
source
@[simp, norm_cast]
theorem nat.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
↑0 = 0
source
theorem nat.cast_add_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
↑(n + 1) = ↑n + 1
source
@[simp, norm_cast]
theorem nat.cast_succ {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
↑(n.succ) = ↑n + 1
source
@[simp, norm_cast]
theorem nat.cast_ite {α : Type u_1} [has_zero α] [has_one α] [has_add α] (P : Prop) [decidable P] (m n : ℕ) :
↑(ite P m n) = ite P ↑m ↑n
source
@[simp, norm_cast]
theorem nat.cast_one {α : Type u_1} [add_zero_class α] [has_one α] :
↑1 = 1
source
@[simp, norm_cast]
theorem nat.cast_add {α : Type u_1} [add_monoid α] [has_one α] (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem nat.bin_cast_eq {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :
n.bin_cast = ↑n
source
def nat.cast_add_monoid_hom (α : Type u_1) [add_monoid α] [has_one α] :
ℕ →+ α

coe : ℕ → α as an add_monoid_hom.

Equations
source
@[simp]
theorem nat.coe_cast_add_monoid_hom {α : Type u_1} [add_monoid α] [has_one α] :
⇑(nat.cast_add_monoid_hom α) = coe
source
@[simp, norm_cast]
theorem nat.cast_bit0 {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :
↑(bit0 n) = bit0 ↑n
source
@[simp, norm_cast]
theorem nat.cast_bit1 {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :
↑(bit1 n) = bit1 ↑n
source
theorem nat.cast_two {α : Type u_1} [add_zero_class α] [has_one α] :
↑2 = 2
source
@[simp, norm_cast]
theorem nat.cast_pred {α : Type u_1} [add_group α] [has_one α] {n : ℕ} :
0 < n → ↑(n - 1) = ↑n - 1
source
@[simp, norm_cast]
theorem nat.cast_sub {α : Type u_1} [add_group α] [has_one α] {m n : ℕ} (h : m ≤ n) :
↑(n - m) = ↑n - ↑m
source
@[simp, norm_cast]
theorem nat.cast_mul {α : Type u_1} [non_assoc_semiring α] (m n : ℕ) :
↑m * n = (↑m) * ↑n
source
@[simp]
theorem nat.cast_dvd {α : Type u_1} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : ↑n ≠ 0) :
↑(m / n) = ↑m / ↑n
source
def nat.cast_ring_hom (α : Type u_1) [non_assoc_semiring α] :
ℕ →+* α

coe : ℕ → α as a ring_hom

Equations
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
@[simp]
theorem nat.cast_nonneg {α : Type u_1} [ordered_semiring α] (n : ℕ) :
0 ≤ ↑n
source
theorem nat.mono_cast {α : Type u_1} [ordered_semiring α] :
monotone coe
source
theorem nat.strict_mono_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] :
strict_mono coe
source
@[simp, norm_cast]
theorem nat.cast_le {α : Type u_1} [ordered_semiring α] [nontrivial α] {m n : ℕ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp, norm_cast]
theorem nat.cast_lt {α : Type u_1} [ordered_semiring α] [nontrivial α] {m n : ℕ} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem nat.cast_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :
0 < ↑n ↔ 0 < n
source
theorem nat.cast_add_one_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] (n : ℕ) :
0 < ↑n + 1
source
@[simp, norm_cast]
theorem nat.one_lt_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :
1 < ↑n ↔ 1 < n
source
@[simp, norm_cast]
theorem nat.one_le_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :
1 ≤ ↑n ↔ 1 ≤ n
source
@[simp, norm_cast]
theorem nat.cast_lt_one {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :
↑n < 1 ↔ n = 0
source
@[simp, norm_cast]
theorem nat.cast_le_one {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : ℕ} :
↑n ≤ 1 ↔ n ≤ 1
source
@[simp, norm_cast]
theorem nat.cast_min {α : Type u_1} [linear_ordered_semiring α] {a b : ℕ} :
↑(min a b) = min ↑a ↑b
source
@[simp, norm_cast]
theorem nat.cast_max {α : Type u_1} [linear_ordered_semiring α] {a b : ℕ} :
↑(max a b) = 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 coe_nat_dvd.

source
theorem nat.cast_div_le {α : Type u_1} [linear_ordered_field α] {m n : ℕ} :
↑(m / n) ≤ ↑m / ↑n

Natural division is always less than division in the field.

source
theorem nat.inv_pos_of_nat {α : Type u_1} [linear_ordered_field α] {n : ℕ} :
0 < (↑n + 1)⁻¹
source
theorem nat.one_div_pos_of_nat {α : Type u_1} [linear_ordered_field α] {n : ℕ} :
0 < 1 / (↑n + 1)
source
theorem nat.one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {n m : ℕ} (h : n ≤ m) :
1 / (↑m + 1) ≤ 1 / (↑n + 1)
source
theorem nat.one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {n m : ℕ} (h : n < m) :
1 / (↑m + 1) < 1 / (↑n + 1)
source
@[simp]
theorem prod.fst_nat_cast {α : Type u_1} {β : Type u_2} [has_zero α] [has_one α] [has_add α] [has_zero β] [has_one β] [has_add β] (n : ℕ) :
↑n.fst = ↑n
source
@[simp]
theorem prod.snd_nat_cast {α : Type u_1} {β : Type u_2} [has_zero α] [has_one α] [has_add α] [has_zero β] [has_one β] [has_add β] (n : ℕ) :
↑n.snd = ↑n
source
theorem ext_nat' {A : Type u_1} {F : Type u_3} [add_zero_class 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_1} [add_zero_class A] {f g : ℕ →+ A} (h : ⇑f 1 = ⇑g 1) :
f = g
source
theorem eq_nat_cast' {A : Type u_1} {F : Type u_3} [add_zero_class A] [has_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_2} {F : Type u_3} [add_monoid B] [has_one B] {A : Type u_1} [add_monoid A] [has_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_1} {F : Type u_2} [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_1} [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_1} {F : Type u_3} [non_assoc_semiring R] [ring_hom_class F ℕ R] (f : F) (n : ℕ) :
⇑f n = ↑n
source
@[simp]
theorem map_nat_cast {R : Type u_1} {S : Type u_2} {F : Type u_3} [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_1} {F : Type u_3} [non_assoc_semiring R] [ring_hom_class F ℕ R] (f g : F) :
f = g
source
theorem ring_hom.eq_nat_cast' {R : Type u_1} [non_assoc_semiring R] (f : ℕ →+* R) :
f = nat.cast_ring_hom R

This is primed to match ring_hom.eq_int_cast'.

source
@[simp, norm_cast]
theorem nat.cast_id (n : ℕ) :
↑n = n
source
@[simp]
theorem nat.cast_ring_hom_nat  :
nat.cast_ring_hom ℕ = ring_hom.id ℕ
source
@[simp]
theorem nat.cast_with_bot (n : ℕ) :
↑n = ↑n
source
@[protected, instance]
def nat.unique_ring_hom {R : Type u_1} [non_assoc_semiring R] :
unique (ℕ →+* R)
Equations
source
@[simp, norm_cast]
theorem mul_opposite.op_nat_cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
mul_opposite.op ↑n = ↑n
source
@[simp, norm_cast]
theorem mul_opposite.unop_nat_cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
mul_opposite.unop ↑n = ↑n
source
@[simp, norm_cast]
theorem with_top.coe_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem with_top.nat_ne_top {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
↑n ≠ ⊤
source
@[simp]
theorem with_top.top_ne_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :
⊤ ≠ ↑n
source
theorem with_top.add_one_le_of_lt {i n : with_top ℕ} (h : i < n) :
i + 1 ≤ n
source
theorem with_top.one_le_iff_pos {n : with_top ℕ} :
1 ≤ n ↔ 0 < n
source
theorem with_top.nat_induction {P : with_top ℕ → Prop} (a : with_top ℕ) (h0 : P 0) (hsuc : ∀ (n : ℕ), P ↑n → P ↑(n.succ)) (htop : (∀ (n : ℕ), P ↑n) → P ⊤) :
P a
source
theorem pi.nat_apply {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] (n : ℕ) (a : α) :
↑n a = ↑n
source
@[simp]
theorem pi.coe_nat {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] (n : ℕ) :
↑n = λ (_x : α), ↑n