# mathlib3documentation

data.nat.cast.basic

# Cast of natural numbers (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 natural numbers into an additive monoid with a one (nat.cast).

## Main declarations #

• cast_add_monoid_hom: cast bundled as an add_monoid_hom.
• cast_ring_hom: cast bundled as a ring_hom.
def nat.cast_add_monoid_hom (α : Type u_1)  :

coe : ℕ → α as an add_monoid_hom.

Equations
@[simp]
theorem nat.coe_cast_add_monoid_hom {α : Type u_1}  :
@[simp, norm_cast]
theorem nat.cast_mul {α : Type u_1} (m n : ) :
(m * n) = m * n
def nat.cast_ring_hom (α : Type u_1)  :

coe : ℕ → α as a ring_hom

Equations
@[simp]
theorem nat.coe_cast_ring_hom {α : Type u_1}  :
theorem nat.cast_commute {α : Type u_1} (n : ) (x : α) :
x
theorem nat.cast_comm {α : Type u_1} (n : ) (x : α) :
n * x = x * n
theorem nat.commute_cast {α : Type u_1} (x : α) (n : ) :
n
theorem nat.mono_cast {α : Type u_1}  :
@[simp]
theorem nat.cast_nonneg {α : Type u_1} (n : ) :
0 n
theorem nat.cast_add_one_pos {α : Type u_1} [nontrivial α] (n : ) :
0 < n + 1
@[simp]
theorem nat.cast_pos {α : Type u_1} [nontrivial α] {n : } :
0 < n 0 < n
theorem nat.strict_mono_cast {α : Type u_1} [char_zero α] :
def nat.cast_order_embedding {α : Type u_1} [char_zero α] :

coe : ℕ → α as an order_embedding

Equations
@[simp]
theorem nat.cast_order_embedding_apply {α : Type u_1} [char_zero α] :
@[simp, norm_cast]
theorem nat.cast_le {α : Type u_1} [char_zero α] {m n : } :
m n m n
@[simp, norm_cast]
theorem nat.cast_lt {α : Type u_1} [char_zero α] {m n : } :
m < n m < n
@[simp, norm_cast]
theorem nat.one_lt_cast {α : Type u_1} [char_zero α] {n : } :
1 < n 1 < n
@[simp, norm_cast]
theorem nat.one_le_cast {α : Type u_1} [char_zero α] {n : } :
1 n 1 n
@[simp, norm_cast]
theorem nat.cast_lt_one {α : Type u_1} [char_zero α] {n : } :
n < 1 n = 0
@[simp, norm_cast]
theorem nat.cast_le_one {α : Type u_1} [char_zero α] {n : } :
n 1 n 1
@[simp, norm_cast]
theorem nat.cast_tsub {α : Type u_1} [has_sub α] (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.

@[simp, norm_cast]
theorem nat.cast_min {α : Type u_1} {a b : } :
b) =
@[simp, norm_cast]
theorem nat.cast_max {α : Type u_1} {a b : } :
b) =
@[simp, norm_cast]
theorem nat.abs_cast {α : Type u_1} (a : ) :
theorem nat.coe_nat_dvd {α : Type u_1} [semiring α] {m n : } (h : m n) :
theorem has_dvd.dvd.nat_cast {α : Type u_1} [semiring α] {m n : } (h : m n) :

Alias of nat.coe_nat_dvd.

theorem ext_nat' {A : Type u_3} {F : Type u_5} [add_monoid A] [ A] (f g : F) (h : f 1 = g 1) :
f = g
@[ext]
theorem add_monoid_hom.ext_nat {A : Type u_3} [add_monoid A] {f g : →+ A} (h : f 1 = g 1) :
f = g
theorem eq_nat_cast' {A : Type u_3} {F : Type u_5} [ A] (f : F) (h1 : f 1 = 1) (n : ) :
f n = n
theorem map_nat_cast' {B : Type u_4} {F : Type u_5} {A : Type u_1} [ B] (f : F) (h : f 1 = 1) (n : ) :
theorem ext_nat'' {A : Type u_3} {F : Type u_4} (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.

@[ext]
theorem monoid_with_zero_hom.ext_nat {A : Type u_3} {f g : →*₀ A} :
( {n : }, 0 < n f n = g n) f = g
@[simp]
theorem eq_nat_cast {R : Type u_3} {F : Type u_5} [ R] (f : F) (n : ) :
f n = n
@[simp]
theorem map_nat_cast {R : Type u_3} {S : Type u_4} {F : Type u_5} [ S] (f : F) (n : ) :
theorem ext_nat {R : Type u_3} {F : Type u_5} [ R] (f g : F) :
f = g
theorem ne_zero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} {n : } [h : ne_zero n] [ S] {f : F} (hf : function.injective f) :
theorem ne_zero.nat_of_ne_zero {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {F : Type u_3} [ S] (f : F) {n : } [hn : ne_zero n] :
theorem ring_hom.eq_nat_cast' {R : Type u_1} (f : →+* R) :

This is primed to match eq_int_cast'.

@[simp, norm_cast]
theorem nat.cast_id (n : ) :
n = n
@[simp]
@[protected, instance]
def nat.unique_ring_hom {R : Type u_1}  :
Equations
@[protected, instance]
def pi.has_nat_cast {α : Type u_1} {π : α Type u_3} [Π (a : α), has_nat_cast (π a)] :
has_nat_cast (Π (a : α), π a)
Equations
theorem pi.nat_apply {α : Type u_1} {π : α Type u_3} [Π (a : α), has_nat_cast (π a)] (n : ) (a : α) :
n a = n
@[simp]
theorem pi.coe_nat {α : Type u_1} {π : α Type u_3} [Π (a : α), has_nat_cast (π a)] (n : ) :
n = λ (_x : α), n
theorem sum.elim_nat_cast_nat_cast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_nat_cast γ] (n : ) :
n = n
@[protected, instance]
def pi.add_monoid_with_one {α : Type u_1} {π : α Type u_3} [Π (a : α), add_monoid_with_one (π a)] :
add_monoid_with_one (Π (a : α), π a)
Equations

### Order dual #

@[protected, instance]
def order_dual.has_nat_cast {α : Type u_1} [h : has_nat_cast α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem to_dual_nat_cast {α : Type u_1} [has_nat_cast α] (n : ) :
@[simp]
theorem of_dual_nat_cast {α : Type u_1} [has_nat_cast α] (n : ) :

### Lexicographic order #

@[protected, instance]
def lex.has_nat_cast {α : Type u_1} [h : has_nat_cast α] :
Equations
@[protected, instance]