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.

theorem Int.cast_mono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] :
Monotone Int.cast
@[simp]
theorem Int.cast_nonneg {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {n : } :
0 n 0 n
@[simp]
theorem Int.cast_le {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {m : } {n : } :
m n m n
theorem Int.cast_strictMono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] :
StrictMono fun (x : ) => x
@[simp]
theorem Int.cast_lt {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {m : } {n : } :
m < n m < n
@[simp]
theorem Int.cast_nonpos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {n : } :
n 0 n 0
@[simp]
theorem Int.cast_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {n : } :
0 < n 0 < n
@[simp]
theorem Int.cast_lt_zero {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [ZeroLEOneClass R] [NeZero 1] {n : } :
n < 0 n < 0
@[simp]
theorem Int.cast_min {R : Type u_1} [LinearOrderedRing R] {a : } {b : } :
(min a b) = min a b
@[simp]
theorem Int.cast_max {R : Type u_1} [LinearOrderedRing R] {a : } {b : } :
(max a b) = max a b
@[simp]
theorem Int.cast_abs {R : Type u_1} [LinearOrderedRing R] {a : } :
|a| = |a|
theorem Int.cast_one_le_of_pos {R : Type u_1} [LinearOrderedRing R] {a : } (h : 0 < a) :
1 a
theorem Int.cast_le_neg_one_of_neg {R : Type u_1} [LinearOrderedRing R] {a : } (h : a < 0) :
a -1
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
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
theorem Int.cast_natAbs {R : Type u_1} [LinearOrderedRing R] {n : } :
n.natAbs = |n|

Order dual #

Equations
  • OrderDual.instIntCast = inst
Equations
  • OrderDual.instAddGroupWithOne = inst
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] :
Equations
  • Lex.instIntCast = inst
Equations
  • Lex.instAddGroupWithOne = inst
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