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.
@[simp]
@[simp]
theorem
Int.cast_strictMono
{R : Type u_1}
[OrderedRing R]
[Nontrivial R]
:
StrictMono fun (x : ℤ) => ↑x
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
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)
:
theorem
Int.nneg_mul_add_sq_of_abs_le_one
{R : Type u_1}
[LinearOrderedRing R]
{x : R}
(n : ℤ)
(hx : |x| ≤ 1)
:
Order dual #
Equations
- OrderDual.instAddGroupWithOne = inst
Equations
- OrderDual.instAddCommGroupWithOne = inst
Lexicographic order #
Equations
- Lex.instAddGroupWithOne = inst
Equations
- Lex.instAddCommGroupWithOne = inst