# Cast of natural numbers: lemmas about order #

theorem Nat.mono_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] :
Monotone Nat.cast
@[deprecated Nat.mono_cast]
theorem Nat.cast_le_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : } {b : } (h : a b) :
a b
theorem GCongr.natCast_le_natCast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : } {b : } (h : a b) :
a b
@[simp]
theorem Nat.cast_nonneg' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] (n : ) :
0 n

See also Nat.cast_nonneg, specialised for an OrderedSemiring.

@[simp]
theorem Nat.cast_nonneg {α : Type u_3} [] (n : ) :
0 n

Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use.

@[simp]
theorem Nat.ofNat_nonneg' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] (n : ) [n.AtLeastTwo] :
0

See also Nat.ofNat_nonneg, specialised for an OrderedSemiring.

@[simp]
theorem Nat.ofNat_nonneg {α : Type u_3} [] (n : ) [n.AtLeastTwo] :
0

Specialisation of Nat.ofNat_nonneg', which seems to be easier for Lean to use.

@[simp]
theorem Nat.cast_min {α : Type u_3} {a : } {b : } :
(min a b) = min a b
@[simp]
theorem Nat.cast_max {α : Type u_3} {a : } {b : } :
(max a b) = max a b
theorem Nat.cast_add_one_pos {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] (n : ) :
0 < n + 1
@[simp]
theorem Nat.cast_pos' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } :
0 < n 0 < n

See also Nat.cast_pos, specialised for an OrderedSemiring.

@[simp]
theorem Nat.cast_pos {α : Type u_3} [] [] {n : } :
0 < n 0 < n

Specialisation of Nat.cast_pos', which seems to be easier for Lean to use.

@[simp]
theorem Nat.ofNat_pos' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } [n.AtLeastTwo] :
0 <

See also Nat.ofNat_pos, specialised for an OrderedSemiring.

@[simp]
theorem Nat.ofNat_pos {α : Type u_3} [] [] {n : } [n.AtLeastTwo] :
0 <

Specialisation of Nat.ofNat_pos', which seems to be easier for Lean to use.

theorem Nat.strictMono_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] :
StrictMono Nat.cast
@[simp]
theorem Nat.castOrderEmbedding_apply {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] :
Nat.castOrderEmbedding = Nat.cast
def Nat.castOrderEmbedding {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] :

Nat.cast : ℕ → α as an OrderEmbedding

Equations
Instances For
@[simp]
theorem Nat.cast_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } :
m n m n
@[simp]
theorem Nat.cast_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } :
m < n m < n
@[simp]
theorem Nat.one_lt_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } :
1 < n 1 < n
@[simp]
theorem Nat.one_le_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } :
1 n 1 n
@[simp]
theorem Nat.cast_lt_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } :
n < 1 n = 0
@[simp]
theorem Nat.cast_le_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } :
n 1 n 1
theorem Nat.ofNat_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [m.AtLeastTwo] [n.AtLeastTwo] :
theorem Nat.ofNat_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [m.AtLeastTwo] [n.AtLeastTwo] :
@[simp]
theorem Nat.ofNat_le_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [m.AtLeastTwo] :
n n
@[simp]
theorem Nat.ofNat_lt_cast {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [m.AtLeastTwo] :
< n < n
@[simp]
theorem Nat.cast_le_ofNat {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [n.AtLeastTwo] :
m m
@[simp]
theorem Nat.cast_lt_ofNat {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {m : } {n : } [n.AtLeastTwo] :
m < m <
@[simp]
theorem Nat.one_lt_ofNat {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } [n.AtLeastTwo] :
1 <
@[simp]
theorem Nat.one_le_ofNat {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } [n.AtLeastTwo] :
1
@[simp]
theorem Nat.not_ofNat_le_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } [n.AtLeastTwo] :
@[simp]
theorem Nat.not_ofNat_lt_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] [] {n : } [n.AtLeastTwo] :
¬ < 1
@[simp]
theorem Nat.cast_tsub {α : Type u_1} [Sub α] [] [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 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

@[simp]
theorem Nat.abs_cast {α : Type u_1} (a : ) :
|a| = a
@[simp]
theorem Nat.abs_ofNat {α : Type u_1} (n : ) [n.AtLeastTwo] :
|| =
instance instNontrivialOfCharZero {α : Type u_1} [] [] :
Equations
• =
theorem NeZero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F R S] {n : } [h : NeZero n] [RingHomClass F R S] {f : F} (hf : ) :
NeZero n