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].

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

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

Equations
@[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
@[protected, instance]
def nat.cast_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
Equations
@[simp, norm_cast]
theorem nat.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
0 = 0
theorem nat.cast_add_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ) :
(n + 1) = n + 1
@[simp, norm_cast]
theorem nat.cast_succ {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ) :
(n.succ) = n + 1
@[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
@[simp, norm_cast]
theorem nat.cast_one {α : Type u_1} [add_monoid α] [has_one α] :
1 = 1
@[simp, norm_cast]
theorem nat.cast_add {α : Type u_1} [add_monoid α] [has_one α] (m n : ) :
(m + n) = m + n
@[simp]
theorem nat.bin_cast_eq {α : Type u_1} [add_monoid α] [has_one α] (n : ) :
def nat.cast_add_monoid_hom (α : Type u_1) [add_monoid α] [has_one α] :

coe : ℕ → α as an add_monoid_hom.

Equations
@[simp]
@[simp, norm_cast]
theorem nat.cast_bit0 {α : Type u_1} [add_monoid α] [has_one α] (n : ) :
@[simp, norm_cast]
theorem nat.cast_bit1 {α : Type u_1} [add_monoid α] [has_one α] (n : ) :
theorem nat.cast_two {α : Type u_1} [add_monoid α] [has_one α] :
2 = 2
@[simp, norm_cast]
theorem nat.cast_pred {α : Type u_1} [add_group α] [has_one α] {n : } :
0 < n(n - 1) = n - 1
@[simp, norm_cast]
theorem nat.cast_sub {α : Type u_1} [add_group α] [has_one α] {m n : } (h : m n) :
(n - m) = n - m
@[simp, norm_cast]
theorem nat.cast_mul {α : Type u_1} [non_assoc_semiring α] (m n : ) :
m * n = (m) * n
@[simp]
theorem nat.cast_dvd {α : Type u_1} [field α] {m n : } (n_dvd : n m) (n_nonzero : n 0) :
(m / n) = m / n
def nat.cast_ring_hom (α : Type u_1) [non_assoc_semiring α] :

coe : ℕ → α as a ring_hom

Equations
@[simp]
theorem nat.coe_cast_ring_hom {α : Type u_1} [non_assoc_semiring α] :
theorem nat.cast_commute {α : Type u_1} [non_assoc_semiring α] (n : ) (x : α) :
theorem nat.cast_comm {α : Type u_1} [non_assoc_semiring α] (n : ) (x : α) :
(n) * x = x * n
theorem nat.commute_cast {α : Type u_1} [semiring α] (x : α) (n : ) :
@[simp]
theorem nat.cast_nonneg {α : Type u_1} [ordered_semiring α] (n : ) :
0 n
theorem nat.mono_cast {α : Type u_1} [ordered_semiring α] :
theorem nat.strict_mono_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] :
@[simp, norm_cast]
theorem nat.cast_le {α : Type u_1} [ordered_semiring α] [nontrivial α] {m n : } :
m n m n
@[simp, norm_cast]
theorem nat.cast_lt {α : Type u_1} [ordered_semiring α] [nontrivial α] {m n : } :
m < n m < n
@[simp]
theorem nat.cast_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : } :
0 < n 0 < n
theorem nat.cast_add_one_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] (n : ) :
0 < n + 1
@[simp, norm_cast]
theorem nat.one_lt_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : } :
1 < n 1 < n
@[simp, norm_cast]
theorem nat.one_le_cast {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : } :
1 n 1 n
@[simp, norm_cast]
theorem nat.cast_lt_one {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : } :
n < 1 n = 0
@[simp, norm_cast]
theorem nat.cast_le_one {α : Type u_1} [ordered_semiring α] [nontrivial α] {n : } :
n 1 n 1
@[simp, norm_cast]
theorem nat.cast_min {α : Type u_1} [linear_ordered_semiring α] {a b : } :
(min a b) = min a b
@[simp, norm_cast]
theorem nat.cast_max {α : Type u_1} [linear_ordered_semiring α] {a b : } :
(max a b) = max a b
@[simp, norm_cast]
theorem nat.abs_cast {α : Type u_1} [linear_ordered_ring α] (a : ) :
theorem nat.coe_nat_dvd {α : Type u_1} [comm_semiring α] {m n : } (h : m n) :
theorem has_dvd.dvd.nat_cast {α : Type u_1} [comm_semiring α] {m n : } (h : m n) :

Alias of coe_nat_dvd.

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.

theorem nat.inv_pos_of_nat {α : Type u_1} [linear_ordered_field α] {n : } :
0 < (n + 1)⁻¹
theorem nat.one_div_pos_of_nat {α : Type u_1} [linear_ordered_field α] {n : } :
0 < 1 / (n + 1)
theorem nat.one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {n m : } (h : n m) :
1 / (m + 1) 1 / (n + 1)
theorem nat.one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {n m : } (h : n < m) :
1 / (m + 1) < 1 / (n + 1)
@[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 : ) :
@[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 : ) :
@[ext]
theorem add_monoid_hom.ext_nat {A : Type u_1} [add_monoid A] {f g : →+ A} (h : f 1 = g 1) :
f = g
theorem add_monoid_hom.eq_nat_cast {A : Type u_1} [add_monoid A] [has_one A] (f : →+ A) (h1 : f 1 = 1) (n : ) :
f n = n
theorem add_monoid_hom.map_nat_cast {A : Type u_1} {B : Type u_2} [add_monoid A] [has_one A] [add_monoid B] [has_one B] (f : A →+ B) (h1 : f 1 = 1) (n : ) :
@[ext]
theorem monoid_with_zero_hom.ext_nat {A : Type u_1} [monoid_with_zero A] {f g : monoid_with_zero_hom A} (h_pos : ∀ {n : }, 0 < nf n = g n) :
f = g

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

@[simp]
theorem ring_hom.eq_nat_cast {R : Type u_1} [non_assoc_semiring R] (f : →+* R) (n : ) :
f n = n
@[simp]
theorem ring_hom.map_nat_cast {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) (n : ) :
theorem ring_hom.ext_nat {R : Type u_1} [non_assoc_semiring R] (f g : →+* R) :
f = g
@[simp, norm_cast]
theorem nat.cast_id (n : ) :
n = n
@[simp]
theorem nat.cast_with_bot (n : ) :
@[protected, instance]
@[simp, norm_cast]
theorem with_top.coe_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ) :
@[simp]
theorem with_top.nat_ne_top {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ) :
@[simp]
theorem with_top.top_ne_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ) :
theorem with_top.add_one_le_of_lt {i n : with_top } (h : i < n) :
i + 1 n
theorem with_top.one_le_iff_pos {n : with_top } :
1 n 0 < n
theorem with_top.nat_induction {P : with_top → Prop} (a : with_top ) (h0 : P 0) (hsuc : ∀ (n : ), P nP (n.succ)) (htop : (∀ (n : ), P n)P ) :
P a
theorem pi.nat_apply {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] (n : ) (a : α) :
n a = n
@[simp]
theorem pi.coe_nat {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] (n : ) :
n = λ (_x : α), n