Documentation

Mathlib.Data.Num.ZNum

Properties of the ZNum representation of integers #

This file was split from Mathlib/Data/Num/Lemmas.lean to keep the former under 1500 lines.

source
@[simp]
theorem ZNum.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
↑0 = 0
source
@[simp]
theorem ZNum.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
↑zero = 0
source
@[simp]
theorem ZNum.cast_one {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
↑1 = 1
source
@[simp]
theorem ZNum.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) :
↑(pos n) = ↑n
source
@[simp]
theorem ZNum.cast_neg {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) :
↑(neg n) = -↑n
source
@[simp]
theorem ZNum.cast_zneg {α : Type u_1} [SubtractionMonoid α] [One α] (n : ZNum) :
↑(-n) = -↑n
source
theorem ZNum.neg_zero :
-0 = 0
source
theorem ZNum.zneg_pos (n : PosNum) :
-pos n = neg n
source
theorem ZNum.zneg_neg (n : PosNum) :
-neg n = pos n
source
theorem ZNum.zneg_zneg (n : ZNum) :
- -n = n
source
theorem ZNum.zneg_bit1 (n : ZNum) :
-n.bit1 = (-n).bitm1
source
theorem ZNum.zneg_bitm1 (n : ZNum) :
-n.bitm1 = (-n).bit1
source
theorem ZNum.zneg_succ (n : ZNum) :
-n.succ = (-n).pred
source
theorem ZNum.zneg_pred (n : ZNum) :
-n.pred = (-n).succ
source
@[simp]
theorem ZNum.abs_to_nat (n : ZNum) :
↑n.abs = (↑n).natAbs
source
@[simp]
theorem ZNum.abs_toZNum (n : Num) :
n.toZNum.abs = n
source
@[simp]
theorem ZNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
↑↑n = ↑n
source
theorem ZNum.bit0_of_bit0 (n : ZNum) :
n + n = n.bit0
source
theorem ZNum.bit1_of_bit1 (n : ZNum) :
n + n + 1 = n.bit1
source
@[simp]
theorem ZNum.cast_bit0 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
↑n.bit0 = ↑n + ↑n
source
@[simp]
theorem ZNum.cast_bit1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
↑n.bit1 = ↑n + ↑n + 1
source
@[simp]
theorem ZNum.cast_bitm1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
↑n.bitm1 = ↑n + ↑n - 1
source
theorem ZNum.add_zero (n : ZNum) :
n + 0 = n
source
theorem ZNum.zero_add (n : ZNum) :
0 + n = n
source
theorem ZNum.add_one (n : ZNum) :
n + 1 = n.succ
source
theorem PosNum.cast_to_znum (n : PosNum) :
↑n = ZNum.pos n
source
theorem PosNum.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m n : PosNum) :
↑(m.sub' n) = ↑m - ↑n
source
theorem PosNum.to_nat_eq_succ_pred (n : PosNum) :
↑n = ↑n.pred' + 1
source
theorem PosNum.to_int_eq_succ_pred (n : PosNum) :
↑n = ↑↑n.pred' + 1
source
@[simp]
theorem Num.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m n : Num) :
↑(m.sub' n) = ↑m - ↑n
source
theorem Num.toZNum_succ (n : Num) :
n.succ.toZNum = n.toZNum.succ
source
theorem Num.toZNumNeg_succ (n : Num) :
n.succ.toZNumNeg = n.toZNumNeg.pred
source
@[simp]
theorem Num.pred_succ (n : ZNum) :
n.pred.succ = n
source
theorem Num.succ_ofInt' (n : ℤ) :
ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1
source
theorem Num.ofInt'_toZNum (n : ℕ) :
(↑n).toZNum = ZNum.ofInt' ↑n
source
theorem Num.mem_ofZNum' {m : Num} {n : ZNum} :
m ∈ ofZNum' n ↔ n = m.toZNum
source
theorem Num.ofZNum'_toNat (n : ZNum) :
castNum <$> ofZNum' n = (↑n).toNat?
source
theorem Num.ofZNum_toNat (n : ZNum) :
↑(ofZNum n) = (↑n).toNat
source
@[simp]
theorem Num.cast_ofZNum {α : Type u_1} [AddMonoidWithOne α] (n : ZNum) :
↑(ofZNum n) = ↑(↑n).toNat
source
@[simp]
theorem Num.sub_to_nat (m n : Num) :
↑(m - n) = ↑m - ↑n
source
@[simp]
theorem ZNum.cast_add {α : Type u_1} [AddGroupWithOne α] (m n : ZNum) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem ZNum.cast_succ {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
↑n.succ = ↑n + 1
source
@[simp]
theorem ZNum.mul_to_int (m n : ZNum) :
↑(m * n) = ↑m * ↑n
source
theorem ZNum.cast_mul {α : Type u_1} [NonAssocRing α] (m n : ZNum) :
↑(m * n) = ↑m * ↑n
source
theorem ZNum.ofInt'_neg (n : ℤ) :
ofInt' (-n) = -ofInt' n
source
theorem ZNum.of_to_int' (n : ZNum) :
ofInt' ↑n = n
source
theorem ZNum.to_int_inj {m n : ZNum} :
↑m = ↑n ↔ m = n
source
theorem ZNum.cmp_to_int (m n : ZNum) :
Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
source
theorem ZNum.lt_to_int {m n : ZNum} :
↑m < ↑n ↔ m < n
source
theorem ZNum.le_to_int {m n : ZNum} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem ZNum.cast_lt {α : Type u_1} [Ring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem ZNum.cast_le {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {m n : ZNum} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem ZNum.cast_inj {α : Type u_1} [Ring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum} :
↑m = ↑n ↔ m = n
source
def ZNum.transfer_rw :
Lean.ParserDescr

This tactic tries to turn an (in)equality about ZNums to one about Ints by rewriting.

example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer_rw
  exact le_add_of_nonneg_right (mul_self_nonneg _)
Equations
Instances For
    source
    def ZNum.transfer :
    Lean.ParserDescr

    This tactic tries to prove (in)equalities about ZNums by transferring them to the Int world and then trying to call simp.

    example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer
  exact mul_self_nonneg _
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance ZNum.linearOrder :
      LinearOrder ZNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance ZNum.addMonoid :
      AddMonoid ZNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance ZNum.addCommGroup :
      AddCommGroup ZNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance ZNum.addMonoidWithOne :
      AddMonoidWithOne ZNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance ZNum.commRing :
      CommRing ZNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance ZNum.nontrivial :
      Nontrivial ZNum
      source
      instance ZNum.zeroLEOneClass :
      ZeroLEOneClass ZNum
      source
      instance ZNum.isOrderedAddMonoid :
      IsOrderedAddMonoid ZNum
      source
      instance ZNum.isStrictOrderedRing :
      IsStrictOrderedRing ZNum
      source
      @[simp]
      theorem ZNum.cast_sub {α : Type u_1} [AddCommGroupWithOne α] (m n : ZNum) :
      ↑(m - n) = ↑m - ↑n
      source
      theorem ZNum.neg_of_int (n : ℤ) :
      ↑(-n) = -↑n
      source
      @[simp]
      theorem ZNum.ofInt'_eq (n : ℤ) :
      ofInt' n = ↑n
      source
      @[simp]
      theorem ZNum.of_nat_toZNum (n : ℕ) :
      (↑n).toZNum = ↑n
      source
      @[simp]
      theorem ZNum.of_to_int (n : ZNum) :
      ↑↑n = n
      source
      theorem ZNum.to_of_int (n : ℤ) :
      ↑↑n = n
      source
      @[simp]
      theorem ZNum.of_nat_toZNumNeg (n : ℕ) :
      (↑n).toZNumNeg = -↑n
      source
      @[simp]
      theorem ZNum.of_intCast {α : Type u_1} [AddGroupWithOne α] (n : ℤ) :
      ↑↑n = ↑n
      source
      @[simp]
      theorem ZNum.of_natCast {α : Type u_1} [AddGroupWithOne α] (n : ℕ) :
      ↑↑n = ↑n
      source
      @[simp]
      theorem ZNum.dvd_to_int (m n : ZNum) :
      ↑m ∣ ↑n ↔ m ∣ n
      source
      theorem PosNum.divMod_to_nat_aux {n d : PosNum} {q r : Num} (h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n) (h₂ : ↑r < 2 * ↑d) :
      ↑(d.divModAux q r).2 + ↑d * ↑(d.divModAux q r).1 = ↑n ∧ ↑(d.divModAux q r).2 < ↑d
      source
      theorem PosNum.divMod_to_nat (d n : PosNum) :
      ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2
      source
      @[simp]
      theorem PosNum.div'_to_nat (n d : PosNum) :
      ↑(n.div' d) = ↑n / ↑d
      source
      @[simp]
      theorem PosNum.mod'_to_nat (n d : PosNum) :
      ↑(n.mod' d) = ↑n % ↑d
      source
      @[simp]
      theorem Num.div_zero (n : Num) :
      n / 0 = 0
      source
      @[simp]
      theorem Num.div_to_nat (n d : Num) :
      ↑(n / d) = ↑n / ↑d
      source
      @[simp]
      theorem Num.mod_zero (n : Num) :
      n % 0 = n
      source
      @[simp]
      theorem Num.mod_to_nat (n d : Num) :
      ↑(n % d) = ↑n % ↑d
      source
      theorem Num.gcd_to_nat_aux {n : ℕ} {a b : Num} :
      a ≤ b → (a * b).natSize ≤ n → ↑(gcdAux n a b) = (↑a).gcd ↑b
      source
      @[simp]
      theorem Num.gcd_to_nat (a b : Num) :
      ↑(a.gcd b) = (↑a).gcd ↑b
      source
      theorem Num.dvd_iff_mod_eq_zero {m n : Num} :
      m ∣ n ↔ n % m = 0
      source
      @[implicit_reducible]
      instance Num.decidableDvd :
      DecidableRel fun (x1 x2 : Num) => x1 ∣ x2
      Equations
      source
      @[implicit_reducible]
      instance PosNum.decidableDvd :
      DecidableRel fun (x1 x2 : PosNum) => x1 ∣ x2
      Equations
      source
      @[simp]
      theorem ZNum.div_zero (n : ZNum) :
      n / 0 = 0
      source
      @[simp]
      theorem ZNum.div_to_int (n d : ZNum) :
      ↑(n / d) = ↑n / ↑d
      source
      @[simp]
      theorem ZNum.mod_to_int (n d : ZNum) :
      ↑(n % d) = ↑n % ↑d
      source
      @[simp]
      theorem ZNum.gcd_to_nat (a b : ZNum) :
      ↑(a.gcd b) = (↑a).gcd ↑b
      source
      theorem ZNum.dvd_iff_mod_eq_zero {m n : ZNum} :
      m ∣ n ↔ n % m = 0
      source
      @[implicit_reducible]
      instance ZNum.decidableDvd :
      DecidableRel fun (x1 x2 : ZNum) => x1 ∣ x2
      Equations