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
๐Ÿ“ coverage
theorem Int.cast_mono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] :
Monotone Int.cast
source
๐Ÿ“ coverage
@[simp]
theorem Int.cast_nonneg {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] {n : โ„ค} :
0 โ‰ค n โ†’ 0 โ‰ค โ†‘n
source
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
theorem Int.cast_strictMono {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1] :
StrictMono fun (x : โ„ค) => โ†‘x
source
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[simp]
theorem Int.cast_min {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : โ„ค} :
โ†‘(min a b) = min โ†‘a โ†‘b
source
๐Ÿ“ coverage
@[simp]
theorem Int.cast_max {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : โ„ค} :
โ†‘(max a b) = max โ†‘a โ†‘b
source
๐Ÿ“ coverage
@[simp]
theorem Int.cast_abs {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : โ„ค} :
โ†‘|a| = |โ†‘a|
source
๐Ÿ“ coverage
theorem Int.cast_one_le_of_pos {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : โ„ค} (h : 0 < a) :
1 โ‰ค โ†‘a
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
@[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 #

source
๐Ÿ”ธ coverage
instance OrderDual.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rแต’แตˆ
Equations
    source
    ๐Ÿ”ธ coverage
    instance OrderDual.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
    AddGroupWithOne Rแต’แตˆ
    Equations
      source
      ๐Ÿ”ธ coverage
      instance OrderDual.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
      AddCommGroupWithOne Rแต’แตˆ
      Equations
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem toDual_intCast {R : Type u_1} [IntCast R] (n : โ„ค) :
        OrderDual.toDual โ†‘n = โ†‘n
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem ofDual_intCast {R : Type u_1} [IntCast R] (n : โ„ค) :
        OrderDual.ofDual โ†‘n = โ†‘n

        Lexicographic order #

        source
        ๐Ÿ”ธ coverage
        instance Lex.instIntCast {R : Type u_1} [IntCast R] :
        IntCast (Lex R)
        Equations
          source
          ๐Ÿ”ธ coverage
          instance Lex.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
          AddGroupWithOne (Lex R)
          Equations
            source
            ๐Ÿ”ธ coverage
            instance Lex.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
            AddCommGroupWithOne (Lex R)
            Equations
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem toLex_intCast {R : Type u_1} [IntCast R] (n : โ„ค) :
              toLex โ†‘n = โ†‘n
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem ofLex_intCast {R : Type u_1} [IntCast R] (n : โ„ค) :
              ofLex โ†‘n = โ†‘n