# Documentation

Mathlib.Data.Nat.Cast.Basic

# Cast of natural numbers (additional theorems) #

This file proves additional properties about the canonical homomorphism from the natural numbers into an additive monoid with a one (Nat.cast).

## Main declarations #

• castAddMonoidHom: cast bundled as an AddMonoidHom.
• castRingHom: cast bundled as a RingHom.
def Nat.castAddMonoidHom (α : Type u_1) [inst : ] :

Nat.cast : ℕ → α→ α as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := Nat.cast, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (m n : ), ↑(m + n) = m + n) }
@[simp]
theorem Nat.coe_castAddMonoidHom {α : Type u_1} [inst : ] :
↑() = Nat.cast
@[simp]
theorem Nat.cast_mul {α : Type u_1} [inst : ] (m : ) (n : ) :
↑(m * n) = m * n
def Nat.castRingHom (α : Type u_1) [inst : ] :

Nat.cast : ℕ → α→ α as a RingHom

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Nat.coe_castRingHom {α : Type u_1} [inst : ] :
↑() = Nat.cast
theorem Nat.cast_commute {α : Type u_1} [inst : ] (n : ) (x : α) :
Commute (n) x
theorem Nat.cast_comm {α : Type u_1} [inst : ] (n : ) (x : α) :
n * x = x * n
theorem Nat.commute_cast {α : Type u_1} [inst : ] (x : α) (n : ) :
Commute x n
theorem Nat.mono_cast {α : Type u_1} [inst : ] :
Monotone Nat.cast
@[simp]
theorem Nat.cast_nonneg {α : Type u_1} [inst : ] (n : ) :
0 n
theorem Nat.cast_add_one_pos {α : Type u_1} [inst : ] [inst : ] (n : ) :
0 < n + 1
@[simp]
theorem Nat.cast_pos {α : Type u_1} [inst : ] [inst : ] {n : } :
0 < n 0 < n
theorem Nat.strictMono_cast {α : Type u_1} [inst : ] [inst : ] :
StrictMono Nat.cast
@[simp]
theorem Nat.castOrderEmbedding_apply {α : Type u_1} [inst : ] [inst : ] :
Nat.castOrderEmbedding.toEmbedding = Nat.cast
def Nat.castOrderEmbedding {α : Type u_1} [inst : ] [inst : ] :

Nat.cast : ℕ → α→ α as an OrderEmbedding

Equations
@[simp]
theorem Nat.cast_le {α : Type u_1} [inst : ] [inst : ] {m : } {n : } :
m n m n
@[simp]
theorem Nat.cast_lt {α : Type u_1} [inst : ] [inst : ] {m : } {n : } :
m < n m < n
@[simp]
theorem Nat.one_lt_cast {α : Type u_1} [inst : ] [inst : ] {n : } :
1 < n 1 < n
@[simp]
theorem Nat.one_le_cast {α : Type u_1} [inst : ] [inst : ] {n : } :
1 n 1 n
@[simp]
theorem Nat.cast_lt_one {α : Type u_1} [inst : ] [inst : ] {n : } :
n < 1 n = 0
@[simp]
theorem Nat.cast_le_one {α : Type u_1} [inst : ] [inst : ] {n : } :
n 1 n 1
@[simp]
theorem Nat.cast_tsub {α : Type u_1} [inst : ] [inst : Sub α] [inst : ] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (m : ) (n : ) :
↑(m - n) = m - n

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

@[simp]
theorem Nat.cast_min {α : Type u_1} [inst : ] {a : } {b : } :
↑(min a b) = min a b
@[simp]
theorem Nat.cast_max {α : Type u_1} [inst : ] {a : } {b : } :
↑(max a b) = max a b
@[simp]
theorem Nat.abs_cast {α : Type u_1} [inst : ] (a : ) :
abs a = a
theorem Nat.coe_nat_dvd {α : Type u_1} [inst : ] {m : } {n : } (h : m n) :
m n
theorem Dvd.dvd.natCast {α : Type u_1} [inst : ] {m : } {n : } (h : m n) :
m n

Alias of Nat.coe_nat_dvd.

instance instNontrivial {α : Type u_1} [inst : ] [inst : ] :
Equations
theorem ext_nat' {A : Type u_1} {F : Type u_2} [inst : ] [inst : ] (f : F) (g : F) (h : f 1 = g 1) :
f = g
theorem AddMonoidHom.ext_nat {A : Type u_1} [inst : ] {f : →+ A} {g : →+ A} :
f 1 = g 1f = g
theorem eq_natCast' {A : Type u_2} {F : Type u_1} [inst : ] [inst : ] (f : F) (h1 : f 1 = 1) (n : ) :
f n = n
theorem map_natCast' {B : Type u_3} {F : Type u_2} [inst : ] {A : Type u_1} [inst : ] [inst : ] (f : F) (h : f 1 = 1) (n : ) :
f n = n
theorem ext_nat'' {A : Type u_2} {F : Type u_1} [inst : ] [inst : ] (f : F) (g : F) (h_pos : ∀ {n : }, 0 < nf n = g n) :
f = g

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

theorem MonoidWithZeroHom.ext_nat {A : Type u_1} [inst : ] {f : →*₀ A} {g : →*₀ A} :
(∀ {n : }, 0 < nf n = g n) → f = g
@[simp]
theorem eq_natCast {R : Type u_2} {F : Type u_1} [inst : ] [inst : ] (f : F) (n : ) :
f n = n
@[simp]
theorem map_natCast {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : ] [inst : ] [inst : RingHomClass F R S] (f : F) (n : ) :
f n = n
theorem ext_nat {R : Type u_2} {F : Type u_1} [inst : ] [inst : ] (f : F) (g : F) :
f = g
theorem NeZero.nat_of_injective {R : Type u_1} {S : Type u_3} {F : Type u_2} [inst : ] [inst : ] {n : } [h : NeZero n] [inst : RingHomClass F R S] {f : F} (hf : ) :
NeZero n
theorem NeZero.nat_of_neZero {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] {F : Type u_3} [inst : RingHomClass F R S] (f : F) {n : } [hn : NeZero n] :
NeZero n
theorem RingHom.eq_natCast' {R : Type u_1} [inst : ] (f : →+* R) :

This is primed to match eq_intCast'.

@[simp]
theorem Nat.cast_id (n : ) :
n = n
instance Nat.uniqueRingHom {R : Type u_1} [inst : ] :

We don't use RingHomClass here, since that might cause type-class slowdown for Subsingleton

Equations
• Nat.uniqueRingHom = { toInhabited := { default := }, uniq := (_ : ∀ (f : →+* R), ) }
instance Pi.natCast {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] :
NatCast ((a : α) → π a)
Equations
• Pi.natCast = { natCast := fun n x => n }
theorem Pi.nat_apply {α : Type u_2} {π : αType u_1} [inst : (a : α) → NatCast (π a)] (n : ) (a : α) :
n a = n
@[simp]
theorem Pi.coe_nat {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] (n : ) :
n = fun x => n
theorem Sum.elim_natCast_natCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] (n : ) :
Sum.elim n n = n

### Order dual #

instance instNatCastOrderDual {α : Type u_1} [h : ] :
Equations
• instNatCastOrderDual = h
instance instAddMonoidWithOneOrderDual {α : Type u_1} [h : ] :
Equations
instance instAddCommMonoidWithOneOrderDual {α : Type u_1} [h : ] :
Equations
@[simp]
theorem toDual_natCast {α : Type u_1} [inst : ] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem ofDual_natCast {α : Type u_1} [inst : ] (n : ) :
↑(OrderDual.ofDual n) = n

### Lexicographic order #

instance instNatCastLex {α : Type u_1} [h : ] :
Equations
• instNatCastLex = h
instance instAddMonoidWithOneLex {α : Type u_1} [h : ] :
Equations