Order properties of cast of integers

This file proves additional properties about the canonical homomorphism from the integers into an additive group with a one (Int.cast), particularly results involving algebraic homomorphisms or the order structure on ℤ which were not available in the import dependencies of Mathlib/Data/Int/Cast/Basic.lean.

TODO

Move order lemmas about Nat.cast, Rat.cast, NNRat.cast here.

theorem Int.cast_mono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] : Monotone Int.cast

@[simp]

theorem Int.cast_nonneg {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] {n : ℤ} : 0 ≤ n → 0 ≤ ↑n

@[simp]

theorem Int.cast_nonneg_iff {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} : 0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem Int.cast_le {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {m n : ℤ} : ↑m ≤ ↑n ↔ m ≤ n

theorem Int.cast_strictMono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] : StrictMono fun (x : ℤ) => ↑x

@[simp]

theorem Int.cast_lt {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {m n : ℤ} : ↑m < ↑n ↔ m < n

theorem Int.GCongr.intCast_strictMono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {m n : ℤ} : m < n → ↑m < ↑n

Alias of the reverse direction of Int.cast_lt.

@[simp]

theorem Int.cast_nonpos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} : ↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem Int.cast_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} : 0 < ↑n ↔ 0 < n

@[simp]

theorem Int.cast_lt_zero {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} : ↑n < 0 ↔ n < 0

@[simp]

theorem Int.cast_min {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ} : ↑(min a b) = min ↑a ↑b

@[simp]

theorem Int.cast_max {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ} : ↑(max a b) = max ↑a ↑b

@[simp]

theorem Int.cast_abs {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} : ↑|a| = |↑a|

theorem Int.cast_one_le_of_pos {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : 0 < a) : 1 ≤ ↑a

theorem Int.cast_le_neg_one_of_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : a < 0) : ↑a ≤ -1

theorem Int.cast_le_neg_one_or_one_le_cast_of_ne_zero (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℤ} (hn : n ≠ 0) : ↑n ≤ -1 ∨ 1 ≤ ↑n

theorem Int.nneg_mul_add_sq_of_abs_le_one {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} (n : ℤ) (hx : |x| ≤ 1) : 0 ≤ ↑n * x + ↑n * ↑n

@[deprecated Nat.cast_natAbs (since := "2025-11-07")]

theorem Int.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ℤ) : ↑n.natAbs = ↑|n|

Alias of Nat.cast_natAbs.

Order dual

instance OrderDual.instIntCast {R : Type u_1} [IntCast R] : IntCast Rᵒᵈ

Equations

• OrderDual.instIntCast = inst✝

instance OrderDual.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] : AddGroupWithOne Rᵒᵈ

Equations

• OrderDual.instAddGroupWithOne = inst✝

instance OrderDual.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] : AddCommGroupWithOne Rᵒᵈ

Equations

• OrderDual.instAddCommGroupWithOne = inst✝

@[simp]

theorem toDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) : OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) : OrderDual.ofDual ↑n = ↑n

Lexicographic order

instance Lex.instIntCast {R : Type u_1} [IntCast R] : IntCast (Lex R)

Equations

• Lex.instIntCast = inst✝

instance Lex.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] : AddGroupWithOne (Lex R)

Equations

• Lex.instAddGroupWithOne = inst✝

instance Lex.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] : AddCommGroupWithOne (Lex R)

Equations

• Lex.instAddCommGroupWithOne = inst✝

@[simp]

theorem toLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) : toLex ↑n = ↑n

@[simp]

theorem ofLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) : ofLex ↑n = ↑n