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.

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
theorem Int.GCongr.intCast_mono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] {m n : ℤ} (hmn : m ≤ n) :
↑m ≤ ↑n
source
@[simp]
theorem Int.cast_nonneg {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
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.

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} [LinearOrderedRing R] {a b : ℤ} :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[simp]
theorem Int.cast_max {R : Type u_1} [LinearOrderedRing R] {a b : ℤ} :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[simp]
theorem Int.cast_abs {R : Type u_1} [LinearOrderedRing R] {a : ℤ} :
↑|a| = |↑a|
source
theorem Int.cast_one_le_of_pos {R : Type u_1} [LinearOrderedRing R] {a : ℤ} (h : 0 < a) :
1 ≤ ↑a
source
theorem Int.cast_le_neg_one_of_neg {R : Type u_1} [LinearOrderedRing 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) [LinearOrderedRing R] {n : ℤ} (hn : n ≠ 0) :
↑n ≤ -1 ∨ 1 ≤ ↑n
source
theorem Int.nneg_mul_add_sq_of_abs_le_one {R : Type u_1} [LinearOrderedRing R] {x : R} (n : ℤ) (hx : |x| ≤ 1) :
0 ≤ ↑n * x + ↑n * ↑n
source
theorem Int.cast_natAbs {R : Type u_1} [LinearOrderedRing R] {n : ℤ} :
↑n.natAbs = ↑|n|

Order dual #

source
instance OrderDual.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rᵒᵈ
Equations
  • OrderDual.instIntCast = inst✝
source
instance OrderDual.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne Rᵒᵈ
Equations
  • OrderDual.instAddGroupWithOne = inst✝
source
instance OrderDual.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rᵒᵈ
Equations
  • OrderDual.instAddCommGroupWithOne = inst✝
source
@[simp]
theorem toDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
OrderDual.toDual ↑n = ↑n
source
@[simp]
theorem ofDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
OrderDual.ofDual ↑n = ↑n

Lexicographic order #

source
instance Lex.instIntCast {R : Type u_1} [IntCast R] :
IntCast (Lex R)
Equations
  • Lex.instIntCast = inst✝
source
instance Lex.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne (Lex R)
Equations
  • Lex.instAddGroupWithOne = inst✝
source
instance Lex.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne (Lex R)
Equations
  • Lex.instAddCommGroupWithOne = inst✝
source
@[simp]
theorem toLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
toLex ↑n = ↑n
source
@[simp]
theorem ofLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
ofLex ↑n = ↑n