Documentation

Mathlib.Data.Nat.Cast.Order

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

See also Nat.cast_nonneg, specialised for an OrderedSemiring.

source
@[simp]
theorem Nat.cast_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) :
0 ≤ ↑n

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

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

See also Nat.cast_pos, a specialisation of this to an OrderedSemiring.

source
@[simp]
theorem Nat.cast_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} :
0 < ↑n ↔ 0 < n

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

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
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
    source
    theorem NeZero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] {n : ℕ} [h : NeZero ↑n] [RingHomClass F R S] {f : F} (hf : Function.Injective ⇑f) :
    NeZero ↑n