mathlib docs: data.nat.cast

source

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

ℕ → α

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

Equations

(n + 1).cast = n.cast + 1
0.cast = 0

source

@[instance]

def nat.cast_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

has_coe_t ℕ α

Equations

nat.cast_coe = {coe := nat.cast _inst_3}

source

@[simp]

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]

theorem nat.cast_succ {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : ℕ) :

↑(n.succ) = ↑n + 1

source

@[simp]

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]

theorem nat.cast_one {α : Type u_1} [add_monoid α] [has_one α] :

↑1 = 1

source

@[simp]

theorem nat.cast_add {α : Type u_1} [add_monoid α] [has_one α] (m n : ℕ) :

↑(m + n) = ↑m + ↑n

source

def nat.cast_add_monoid_hom (α : Type u_1) [add_monoid α] [has_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 α] [has_one α] :

⇑(nat.cast_add_monoid_hom α) = coe

source

@[simp]

theorem nat.cast_bit0 {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :

↑(bit0 n) = bit0 ↑n

source

@[simp]

theorem nat.cast_bit1 {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :

↑(bit1 n) = bit1 ↑n

source

theorem nat.cast_two {α : Type u_1} [semiring α] :

↑2 = 2

source

@[simp]

theorem nat.cast_pred {α : Type u_1} [add_group α] [has_one α] {n : ℕ} :

0 < n → ↑(n - 1) = ↑n - 1

source

@[simp]

theorem nat.cast_sub {α : Type u_1} [add_group α] [has_one α] {m n : ℕ} :

m ≤ n → ↑(n - m) = ↑n - ↑m

source

@[simp]

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

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

source

@[simp]

theorem nat.cast_dvd {α : Type u_1} [field α] {m n : ℕ} :

n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n

source

def nat.cast_ring_hom (α : Type u_1) [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} [semiring α] :

⇑(nat.cast_ring_hom α) = coe

source

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

commute ↑n x

source

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

commute x ↑n

source

@[simp]

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

0 ≤ ↑n

source

@[simp]

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

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

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

↑m < ↑n ↔ m < n

source

@[simp]

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

0 < ↑n ↔ 0 < n

source

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

0 < ↑n + 1

source

@[simp]

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

↑(min a b) = min ↑a ↑b

source

@[simp]

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

↑(max a b) = max ↑a ↑b

source

@[simp]

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

abs ↑a = ↑a

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 : ℕ} :

n ≤ m → 1 / (↑m + 1) ≤ 1 / (↑n + 1)

source

theorem nat.one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {n m : ℕ} :

n < m → 1 / (↑m + 1) < 1 / (↑n + 1)

source

@[ext]

theorem add_monoid_hom.ext_nat {A : Type u_1} [add_monoid A] {f g : ℕ →+ A} :

⇑f 1 = ⇑g 1 → f = g

source

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

source

@[simp]

theorem ring_hom.eq_nat_cast {R : Type u_1} [semiring R] (f : ℕ →+* R) (n : ℕ) :

⇑f n = ↑n

source

@[simp]

theorem ring_hom.map_nat_cast {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) (n : ℕ) :

⇑f ↑n = ↑n

source

theorem ring_hom.ext_nat {R : Type u_1} [semiring R] (f g : ℕ →+* R) :

f = g

source

@[simp]

theorem nat.cast_id (n : ℕ) :

↑n = n

source

@[simp]

theorem nat.cast_with_bot (n : ℕ) :

↑n = ↑n

source

@[instance]

def nat.subsingleton_ring_hom {R : Type u_1} [semiring R] :

subsingleton (ℕ →+* R)

Equations

nat.subsingleton_ring_hom = _

source

@[simp]

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 ℕ} :

i < n → i + 1 ≤ n

source

theorem with_top.nat_induction {P : with_top ℕ → Prop} (a : with_top ℕ) :

P 0 → (∀ (n : ℕ), P ↑n → P ↑(n.succ)) → ((∀ (n : ℕ), P ↑n) → P ⊤) → P a

mathlib documentation

data.nat.cast

General documentation

Additional documentation

Library

mathlib documentation

data.​nat.​cast

General documentation

Additional documentation

Library

data.nat.cast