Documentation

Mathlib.Algebra.Order.Ring.Cast

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.

source
theorem Int.cast_mono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] :
Monotone Int.cast
source
@[simp]
theorem Int.cast_nonneg {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] {n : ℤ} :
0 ≤ n → 0 ≤ ↑n
source
@[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
source
@[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
source
theorem Int.cast_strictMono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] :
StrictMono fun (x : ℤ) => ↑x
source
@[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
source
@[simp]
theorem Int.cast_nonpos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} :
↑n ≤ 0 ↔ n ≤ 0
source
@[simp]
theorem Int.cast_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] {n : ℤ} :
0 < ↑n ↔ 0 < n
source
@[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
source
@[simp]
theorem Int.cast_min {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ} :
↑(min a b) = min ↑a ↑b
source
@[simp]
theorem Int.cast_max {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ} :
↑(max a b) = max ↑a ↑b
source
@[simp]
theorem Int.cast_abs {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} :
↑|a| = |↑a|
source
theorem Int.cast_one_le_of_pos {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : 0 < a) :
1 ≤ ↑a
source
theorem Int.cast_le_neg_one_of_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} (h : a < 0) :
↑a ≤ -1
source
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
source
theorem Int.nonneg_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
source
@[deprecated Int.nonneg_mul_add_sq_of_abs_le_one (since := "2026-09-17")]
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

Alias of Int.nonneg_mul_add_sq_of_abs_le_one.