Cast of natural numbers: lemmas about order #

source

theorem Nat.mono_cast {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] :

Monotone Nat.cast

source

@[simp]

theorem Nat.cast_nonneg' {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] (n : ℕ) :

0 ≤ ↑n

source

@[simp]

theorem Nat.cast_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) :

0 ≤ ↑n

source

@[simp]

theorem Nat.cast_min {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

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

source

@[simp]

theorem Nat.cast_max {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

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

source

theorem Nat.cast_add_one_pos {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] (n : ℕ) :

0 < ↑n + 1

source

@[simp]

theorem Nat.cast_pos' {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} :

0 < ↑n ↔ 0 < n

source

@[simp]

theorem Nat.cast_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} :

0 < ↑n ↔ 0 < n

source

theorem Nat.strictMono_cast {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

StrictMono Nat.cast

source

@[simp]

theorem Nat.castOrderEmbedding_apply {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

↑Nat.castOrderEmbedding = Nat.cast

source

def Nat.castOrderEmbedding {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

ℕ ↪o α

Nat.cast : ℕ → α as an OrderEmbedding

Equations

Nat.castOrderEmbedding = OrderEmbedding.ofStrictMono Nat.cast (_ : StrictMono Nat.cast)

Instances For

source

@[simp]

theorem Nat.cast_le {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

theorem Nat.cast_lt {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} :

↑m < ↑n ↔ m < n

source

@[simp]

theorem Nat.one_lt_cast {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

1 < ↑n ↔ 1 < n

source

@[simp]

theorem Nat.one_le_cast {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

1 ≤ ↑n ↔ 1 ≤ n

source

@[simp]

theorem Nat.cast_lt_one {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

↑n < 1 ↔ n = 0

source

@[simp]

theorem Nat.cast_le_one {α : Type u_1} [AddCommMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

↑n ≤ 1 ↔ n ≤ 1

source

@[simp]

theorem Nat.cast_tsub {α : Type u_1} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [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.

source

@[simp]

theorem Nat.abs_cast {α : Type u_1} [LinearOrderedRing α] (a : ℕ) :

|↑a| = ↑a

source

instance instNontrivial {α : Type u_1} [AddMonoidWithOne α] [CharZero α] :

Nontrivial α

Equations

@instNontrivial = @instNontrivial.proof_1

source

theorem NeZero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] {n : ℕ} [h : NeZero ↑n] [RingHomClass F R S] {f : F} (hf : Function.Injective ↑f) :

NeZero ↑n