# Cast of natural numbers: lemmas about order #

source
theorem Nat.mono_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] :
Monotone Nat.cast
source
@[simp]
theorem Nat.cast_nonneg' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) :
0 ≤ ↑n

See also `Nat.cast_nonneg`, specialised for an `OrderedSemiring`.

source
@[simp]
theorem Nat.ofNat_nonneg' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) [n.AtLeastTwo] :
0 ≤ OfNat.ofNat n

See also `Nat.ofNat_nonneg`, specialised for an `OrderedSemiring`.

source
theorem Nat.cast_add_one_pos {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1] (n : ℕ) :
0 < ↑n + 1
source
@[simp]
theorem Nat.cast_pos' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} :
0 < ↑n ↔ 0 < n

See also `Nat.cast_pos`, specialised for an `OrderedSemiring`.

source
theorem Nat.strictMono_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
StrictMono Nat.cast
source
def Nat.castOrderEmbedding {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
ℕ ↪o α

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

Equations

- Nat.castOrderEmbedding = OrderEmbedding.ofStrictMono Nat.cast ⋯

Instances For

source
@[simp]
theorem Nat.castOrderEmbedding_apply {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
⇑castOrderEmbedding = Nat.cast
source
@[simp]
theorem Nat.cast_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem Nat.cast_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem Nat.one_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
1 < ↑n ↔ 1 < n
source
@[simp]
theorem Nat.one_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
1 ≤ ↑n ↔ 1 ≤ n
source
theorem Nat.one_le_cast_iff_ne_zero {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
1 ≤ ↑n ↔ n ≠ 0
source
@[simp]
theorem Nat.cast_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
↑n < 1 ↔ n = 0
source
@[simp]
theorem Nat.cast_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
↑n ≤ 1 ↔ n ≤ 1
source
@[simp]
theorem Nat.cast_nonpos {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :
↑n ≤ 0 ↔ n = 0
source
@[simp]
theorem Nat.ofNat_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [m.AtLeastTwo] :
OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
source
@[simp]
theorem Nat.ofNat_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [m.AtLeastTwo] :
OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
source
@[simp]
theorem Nat.cast_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [n.AtLeastTwo] :
↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
source
@[simp]
theorem Nat.cast_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [n.AtLeastTwo] :
↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
source
@[simp]
theorem Nat.one_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [n.AtLeastTwo] :
1 < OfNat.ofNat n
source
@[simp]
theorem Nat.one_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [n.AtLeastTwo] :
1 ≤ OfNat.ofNat n
source
@[simp]
theorem Nat.not_ofNat_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [n.AtLeastTwo] :
¬OfNat.ofNat n ≤ 1
source
@[simp]
theorem Nat.not_ofNat_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [n.AtLeastTwo] :
¬OfNat.ofNat n < 1
source
theorem Nat.ofNat_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [n.AtLeastTwo] [m.AtLeastTwo] :
OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
source
theorem Nat.ofNat_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {m n : ℕ} [n.AtLeastTwo] [m.AtLeastTwo] :
OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
source
instance instNontrivialOfCharZero {α : Type u_1} [AddMonoidWithOne α] [CharZero α] :
Nontrivial α
source
theorem NeZero.nat_of_injective {R : Type u_2} {S : Type u_3} {F : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] {n : ℕ} [NeZero ↑n] [RingHomClass F R S] {f : F} (hf : Function.Injective ⇑f) :
NeZero ↑n