Documentation

Mathlib.Data.Nat.Cast.Order.Basic

Cast of natural numbers: lemmas about order #

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

See also Nat.cast_nonneg, specialised for an OrderedSemiring.

@[simp]
theorem Nat.ofNat_nonneg' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] (n : ) [n.AtLeastTwo] :

See also Nat.ofNat_nonneg, specialised for an OrderedSemiring.

theorem Nat.cast_add_one_pos {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [NeZero 1] (n : ) :
0 < n + 1
@[simp]
theorem Nat.cast_pos' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [NeZero 1] {n : } :
0 < n 0 < n

See also Nat.cast_pos, specialised for an OrderedSemiring.

theorem Nat.strictMono_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] :
StrictMono Nat.cast
theorem GCongr.natCast_lt_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {a : } {b : } (h : a < b) :
a < b
@[simp]
theorem Nat.castOrderEmbedding_apply {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] :
Nat.castOrderEmbedding = Nat.cast
def Nat.castOrderEmbedding {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] :

Nat.cast : ℕ → α as an OrderEmbedding

Equations
Instances For
    @[simp]
    theorem Nat.cast_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } :
    m n m n
    @[simp]
    theorem Nat.cast_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } :
    m < n m < n
    @[simp]
    theorem Nat.one_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } :
    1 < n 1 < n
    @[simp]
    theorem Nat.one_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } :
    1 n 1 n
    @[simp]
    theorem Nat.cast_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } :
    n < 1 n = 0
    @[simp]
    theorem Nat.cast_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } :
    n 1 n 1
    @[simp]
    theorem Nat.ofNat_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [m.AtLeastTwo] :
    @[simp]
    theorem Nat.ofNat_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [m.AtLeastTwo] :
    @[simp]
    theorem Nat.cast_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Nat.cast_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Nat.one_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Nat.one_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Nat.not_ofNat_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Nat.not_ofNat_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {n : } [n.AtLeastTwo] :
    theorem Nat.ofNat_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [n.AtLeastTwo] [m.AtLeastTwo] :
    theorem Nat.ofNat_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] [CharZero α] {m : } {n : } [n.AtLeastTwo] [m.AtLeastTwo] :
    Equations
    • =
    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