mathlib3 documentation

data.num.lemmas

Properties of the binary representation of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp, norm_cast]
theorem pos_num.cast_one {α : Type u_1} [has_one α] [has_add α] :
↑1 = 1
source
@[simp]
theorem pos_num.cast_one' {α : Type u_1} [has_one α] [has_add α] :
↑pos_num.one = 1
source
@[simp, norm_cast]
theorem pos_num.cast_bit0 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :
↑(n.bit0) = bit0 ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_bit1 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :
↑(n.bit1) = bit1 ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_to_nat {α : Type u_1} [add_monoid_with_one α] (n : pos_num) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem pos_num.to_nat_to_int (n : pos_num) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_to_int {α : Type u_1} [add_group_with_one α] (n : pos_num) :
↑↑n = ↑n
source
theorem pos_num.succ_to_nat (n : pos_num) :
↑(n.succ) = ↑n + 1
source
theorem pos_num.one_add (n : pos_num) :
1 + n = n.succ
source
theorem pos_num.add_one (n : pos_num) :
n + 1 = n.succ
source
@[norm_cast]
theorem pos_num.add_to_nat (m n : pos_num) :
↑(m + n) = ↑m + ↑n
source
theorem pos_num.add_succ (m n : pos_num) :
m + n.succ = (m + n).succ
source
theorem pos_num.bit0_of_bit0 (n : pos_num) :
bit0 n = n.bit0
source
theorem pos_num.bit1_of_bit1 (n : pos_num) :
bit1 n = n.bit1
source
@[norm_cast]
theorem pos_num.mul_to_nat (m n : pos_num) :
↑(m * n) = ↑m * ↑n
source
theorem pos_num.to_nat_pos (n : pos_num) :
0 < ↑n
source
theorem pos_num.cmp_to_nat_lemma {m n : pos_num} :
↑m < ↑n → ↑(m.bit1) < ↑(n.bit0)
source
theorem pos_num.cmp_swap (m n : pos_num) :
(m.cmp n).swap = n.cmp m
source
theorem pos_num.cmp_to_nat (m n : pos_num) :
(m.cmp n).cases_on (↑m < ↑n) (m = n) (↑n < ↑m)
source
@[norm_cast]
theorem pos_num.lt_to_nat {m n : pos_num} :
↑m < ↑n ↔ m < n
source
@[norm_cast]
theorem pos_num.le_to_nat {m n : pos_num} :
↑m ≤ ↑n ↔ m ≤ n
source
theorem num.add_zero (n : num) :
n + 0 = n
source
theorem num.zero_add (n : num) :
0 + n = n
source
theorem num.add_one (n : num) :
n + 1 = n.succ
source
theorem num.add_succ (m n : num) :
m + n.succ = (m + n).succ
source
theorem num.bit0_of_bit0 (n : num) :
bit0 n = n.bit0
source
theorem num.bit1_of_bit1 (n : num) :
bit1 n = n.bit1
source
@[simp]
theorem num.of_nat'_zero  :
num.of_nat' 0 = 0
source
theorem num.of_nat'_bit (b : bool) (n : ℕ) :
num.of_nat' (nat.bit b n) = cond b num.bit1 num.bit0 (num.of_nat' n)
source
@[simp]
theorem num.of_nat'_one  :
num.of_nat' 1 = 1
source
theorem num.bit1_succ (n : num) :
n.bit1.succ = n.succ.bit0
source
theorem num.of_nat'_succ {n : ℕ} :
num.of_nat' (n + 1) = num.of_nat' n + 1
source
@[simp]
theorem num.add_of_nat' (m n : ℕ) :
num.of_nat' (m + n) = num.of_nat' m + num.of_nat' n
source
@[simp, norm_cast]
theorem num.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
↑0 = 0
source
@[simp]
theorem num.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
↑num.zero = 0
source
@[simp, norm_cast]
theorem num.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
↑1 = 1
source
@[simp]
theorem num.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : pos_num) :
↑(num.pos n) = ↑n
source
theorem num.succ'_to_nat (n : num) :
↑(n.succ') = ↑n + 1
source
theorem num.succ_to_nat (n : num) :
↑(n.succ) = ↑n + 1
source
@[simp, norm_cast]
theorem num.cast_to_nat {α : Type u_1} [add_monoid_with_one α] (n : num) :
↑↑n = ↑n
source
@[norm_cast]
theorem num.add_to_nat (m n : num) :
↑(m + n) = ↑m + ↑n
source
@[norm_cast]
theorem num.mul_to_nat (m n : num) :
↑(m * n) = ↑m * ↑n
source
theorem num.cmp_to_nat (m n : num) :
(m.cmp n).cases_on (↑m < ↑n) (m = n) (↑n < ↑m)
source
@[norm_cast]
theorem num.lt_to_nat {m n : num} :
↑m < ↑n ↔ m < n
source
@[norm_cast]
theorem num.le_to_nat {m n : num} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem pos_num.of_to_nat' (n : pos_num) :
num.of_nat' ↑n = num.pos n
source
@[simp, norm_cast]
theorem num.of_to_nat' (n : num) :
num.of_nat' ↑n = n
source
@[norm_cast]
theorem num.to_nat_inj {m n : num} :
↑m = ↑n ↔ m = n
source
meta def num.transfer_rw  :
tactic unit

This tactic tries to turn an (in)equality about nums to one about nats by rewriting.

example (n : num) (m : num) : n ≤ n + m :=
begin
  num.transfer_rw,
  exact nat.le_add_right _ _
end
source
meta def num.transfer  :
tactic unit

This tactic tries to prove (in)equalities about nums by transfering them to the nat world and then trying to call simp.

example (n : num) (m : num) : n ≤ n + m := by num.transfer
source
@[protected, instance]
def num.add_monoid  :
add_monoid num
Equations
source
@[protected, instance]
def num.add_monoid_with_one  :
add_monoid_with_one num
Equations
source
@[protected, instance]
def num.comm_semiring  :
comm_semiring num
Equations
source
@[protected, instance]
def num.ordered_cancel_add_comm_monoid  :
ordered_cancel_add_comm_monoid num
Equations
source
@[protected, instance]
def num.linear_ordered_semiring  :
linear_ordered_semiring num
Equations
source
@[simp, norm_cast]
theorem num.add_of_nat (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[simp, norm_cast]
theorem num.to_nat_to_int (n : num) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem num.cast_to_int {α : Type u_1} [add_group_with_one α] (n : num) :
↑↑n = ↑n
source
theorem num.to_of_nat (n : ℕ) :
↑↑n = n
source
@[simp, norm_cast]
theorem num.of_nat_cast {α : Type u_1} [add_monoid_with_one α] (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem num.of_nat_inj {m n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp, norm_cast]
theorem num.of_to_nat (n : num) :
↑↑n = n
source
@[norm_cast]
theorem num.dvd_to_nat (m n : num) :
↑m ∣ ↑n ↔ m ∣ n
source
@[simp, norm_cast]
theorem pos_num.of_to_nat (n : pos_num) :
↑↑n = num.pos n
source
@[norm_cast]
theorem pos_num.to_nat_inj {m n : pos_num} :
↑m = ↑n ↔ m = n
source
theorem pos_num.pred'_to_nat (n : pos_num) :
↑(n.pred') = ↑n.pred
source
@[simp]
theorem pos_num.pred'_succ' (n : num) :
n.succ'.pred' = n
source
@[simp]
theorem pos_num.succ'_pred' (n : pos_num) :
n.pred'.succ' = n
source
@[protected, instance]
def pos_num.has_dvd  :
has_dvd pos_num
Equations
source
@[norm_cast]
theorem pos_num.dvd_to_nat {m n : pos_num} :
↑m ∣ ↑n ↔ m ∣ n
source
theorem pos_num.size_to_nat (n : pos_num) :
↑(n.size) = ↑n.size
source
theorem pos_num.size_eq_nat_size (n : pos_num) :
↑(n.size) = n.nat_size
source
theorem pos_num.nat_size_to_nat (n : pos_num) :
n.nat_size = ↑n.size
source
theorem pos_num.nat_size_pos (n : pos_num) :
0 < n.nat_size
source
meta def pos_num.transfer_rw  :
tactic unit

This tactic tries to turn an (in)equality about pos_nums to one about nats by rewriting.

example (n : pos_num) (m : pos_num) : n ≤ n + m :=
begin
  pos_num.transfer_rw,
  exact nat.le_add_right _ _
end
source
meta def pos_num.transfer  :
tactic unit

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

example (n : pos_num) (m : pos_num) : n ≤ n + m := by pos_num.transfer
source
@[protected, instance]
def pos_num.add_comm_semigroup  :
add_comm_semigroup pos_num
Equations
source
@[protected, instance]
def pos_num.comm_monoid  :
comm_monoid pos_num
Equations
source
@[protected, instance]
def pos_num.distrib  :
distrib pos_num
Equations
source
@[protected, instance]
def pos_num.linear_order  :
linear_order pos_num
Equations
source
@[simp]
theorem pos_num.cast_to_num (n : pos_num) :
↑n = num.pos n
source
@[simp, norm_cast]
theorem pos_num.bit_to_nat (b : bool) (n : pos_num) :
↑(pos_num.bit b n) = nat.bit b ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_add {α : Type u_1} [add_monoid_with_one α] (m n : pos_num) :
↑(m + n) = ↑m + ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_succ {α : Type u_1} [add_monoid_with_one α] (n : pos_num) :
↑(n.succ) = ↑n + 1
source
@[simp, norm_cast]
theorem pos_num.cast_inj {α : Type u_1} [add_monoid_with_one α] [char_zero α] {m n : pos_num} :
↑m = ↑n ↔ m = n
source
@[simp]
theorem pos_num.one_le_cast {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :
1 ≤ ↑n
source
@[simp]
theorem pos_num.cast_pos {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :
0 < ↑n
source
@[simp, norm_cast]
theorem pos_num.cast_mul {α : Type u_1} [semiring α] (m n : pos_num) :
↑(m * n) = ↑m * ↑n
source
@[simp]
theorem pos_num.cmp_eq (m n : pos_num) :
m.cmp n = ordering.eq ↔ m = n
source
@[simp, norm_cast]
theorem pos_num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :
↑m < ↑n ↔ m < n
source
@[simp, norm_cast]
theorem pos_num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :
↑m ≤ ↑n ↔ m ≤ n
source
theorem num.bit_to_nat (b : bool) (n : num) :
↑(num.bit b n) = nat.bit b ↑n
source
theorem num.cast_succ' {α : Type u_1} [add_monoid_with_one α] (n : num) :
↑(n.succ') = ↑n + 1
source
theorem num.cast_succ {α : Type u_1} [add_monoid_with_one α] (n : num) :
↑(n.succ) = ↑n + 1
source
@[simp, norm_cast]
theorem num.cast_add {α : Type u_1} [semiring α] (m n : num) :
↑(m + n) = ↑m + ↑n
source
@[simp, norm_cast]
theorem num.cast_bit0 {α : Type u_1} [semiring α] (n : num) :
↑(n.bit0) = bit0 ↑n
source
@[simp, norm_cast]
theorem num.cast_bit1 {α : Type u_1} [semiring α] (n : num) :
↑(n.bit1) = bit1 ↑n
source
@[simp, norm_cast]
theorem num.cast_mul {α : Type u_1} [semiring α] (m n : num) :
↑(m * n) = ↑m * ↑n
source
theorem num.size_to_nat (n : num) :
↑(n.size) = ↑n.size
source
theorem num.size_eq_nat_size (n : num) :
↑(n.size) = n.nat_size
source
theorem num.nat_size_to_nat (n : num) :
n.nat_size = ↑n.size
source
@[simp]
theorem num.of_nat'_eq (n : ℕ) :
num.of_nat' n = ↑n
source
theorem num.zneg_to_znum (n : num) :
-n.to_znum = n.to_znum_neg
source
theorem num.zneg_to_znum_neg (n : num) :
-n.to_znum_neg = n.to_znum
source
theorem num.to_znum_inj {m n : num} :
m.to_znum = n.to_znum ↔ m = n
source
@[simp, norm_cast]
theorem num.cast_to_znum {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : num) :
↑(n.to_znum) = ↑n
source
@[simp]
theorem num.cast_to_znum_neg {α : Type u_1} [add_group α] [has_one α] (n : num) :
↑(n.to_znum_neg) = -↑n
source
@[simp]
theorem num.add_to_znum (m n : num) :
(m + n).to_znum = m.to_znum + n.to_znum
source
theorem pos_num.pred_to_nat {n : pos_num} (h : 1 < n) :
↑(n.pred) = ↑n.pred
source
theorem pos_num.sub'_one (a : pos_num) :
a.sub' 1 = a.pred'.to_znum
source
theorem pos_num.one_sub' (a : pos_num) :
1.sub' a = a.pred'.to_znum_neg
source
theorem pos_num.lt_iff_cmp {m n : pos_num} :
m < n ↔ m.cmp n = ordering.lt
source
theorem pos_num.le_iff_cmp {m n : pos_num} :
m ≤ n ↔ m.cmp n ≠ ordering.gt
source
theorem num.pred_to_nat (n : num) :
↑(n.pred) = ↑n.pred
source
theorem num.ppred_to_nat (n : num) :
coe <$> n.ppred = ↑n.ppred
source
theorem num.cmp_swap (m n : num) :
(m.cmp n).swap = n.cmp m
source
theorem num.cmp_eq (m n : num) :
m.cmp n = ordering.eq ↔ m = n
source
@[simp, norm_cast]
theorem num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
↑m < ↑n ↔ m < n
source
@[simp, norm_cast]
theorem num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp, norm_cast]
theorem num.cast_inj {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
↑m = ↑n ↔ m = n
source
theorem num.lt_iff_cmp {m n : num} :
m < n ↔ m.cmp n = ordering.lt
source
theorem num.le_iff_cmp {m n : num} :
m ≤ n ↔ m.cmp n ≠ ordering.gt
source
theorem num.bitwise_to_nat {f : num → num → num} {g : bool → bool → bool} (p : pos_num → pos_num → num) (gff : g bool.ff bool.ff = bool.ff) (f00 : f 0 0 = 0) (f0n : ∀ (n : pos_num), f 0 (num.pos n) = cond (g bool.ff bool.tt) (num.pos n) 0) (fn0 : ∀ (n : pos_num), f (num.pos n) 0 = cond (g bool.tt bool.ff) (num.pos n) 0) (fnn : ∀ (m n : pos_num), f (num.pos m) (num.pos n) = p m n) (p11 : p 1 1 = cond (g bool.tt bool.tt) 1 0) (p1b : ∀ (b : bool) (n : pos_num), p 1 (pos_num.bit b n) = num.bit (g bool.tt b) (cond (g bool.ff bool.tt) (num.pos n) 0)) (pb1 : ∀ (a : bool) (m : pos_num), p (pos_num.bit a m) 1 = num.bit (g a bool.tt) (cond (g bool.tt bool.ff) (num.pos m) 0)) (pbb : ∀ (a b : bool) (m n : pos_num), p (pos_num.bit a m) (pos_num.bit b n) = num.bit (g a b) (p m n)) (m n : num) :
↑(f m n) = nat.bitwise g ↑m ↑n
source
@[simp, norm_cast]
theorem num.lor_to_nat (m n : num) :
↑(m.lor n) = ↑m.lor ↑n
source
@[simp, norm_cast]
theorem num.land_to_nat (m n : num) :
↑(m.land n) = ↑m.land ↑n
source
@[simp, norm_cast]
theorem num.ldiff_to_nat (m n : num) :
↑(m.ldiff n) = ↑m.ldiff ↑n
source
@[simp, norm_cast]
theorem num.lxor_to_nat (m n : num) :
↑(m.lxor n) = ↑m.lxor ↑n
source
@[simp, norm_cast]
theorem num.shiftl_to_nat (m : num) (n : ℕ) :
↑(m.shiftl n) = ↑m.shiftl n
source
@[simp, norm_cast]
theorem num.shiftr_to_nat (m : num) (n : ℕ) :
↑(m.shiftr n) = ↑m.shiftr n
source
@[simp]
theorem num.test_bit_to_nat (m : num) (n : ℕ) :
m.test_bit n = ↑m.test_bit n
source
@[simp, norm_cast]
theorem znum.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
↑0 = 0
source
@[simp]
theorem znum.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
↑znum.zero = 0
source
@[simp, norm_cast]
theorem znum.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
↑1 = 1
source
@[simp]
theorem znum.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :
↑(znum.pos n) = ↑n
source
@[simp]
theorem znum.cast_neg {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :
↑(znum.neg n) = -↑n
source
@[simp, norm_cast]
theorem znum.cast_zneg {α : Type u_1} [add_group α] [has_one α] (n : znum) :
↑-n = -↑n
source
theorem znum.neg_zero  :
-0 = 0
source
theorem znum.zneg_pos (n : pos_num) :
-znum.pos n = znum.neg n
source
theorem znum.zneg_neg (n : pos_num) :
-znum.neg n = znum.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.nat_abs
source
@[simp]
theorem znum.abs_to_znum (n : num) :
n.to_znum.abs = n
source
@[simp, norm_cast]
theorem znum.cast_to_int {α : Type u_1} [add_group_with_one α] (n : znum) :
↑↑n = ↑n
source
theorem znum.bit0_of_bit0 (n : znum) :
bit0 n = n.bit0
source
theorem znum.bit1_of_bit1 (n : znum) :
bit1 n = n.bit1
source
@[simp, norm_cast]
theorem znum.cast_bit0 {α : Type u_1} [add_group_with_one α] (n : znum) :
↑(n.bit0) = bit0 ↑n
source
@[simp, norm_cast]
theorem znum.cast_bit1 {α : Type u_1} [add_group_with_one α] (n : znum) :
↑(n.bit1) = bit1 ↑n
source
@[simp]
theorem znum.cast_bitm1 {α : Type u_1} [add_group_with_one α] (n : znum) :
↑(n.bitm1) = bit0 ↑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 pos_num.cast_to_znum (n : pos_num) :
↑n = znum.pos n
source
theorem pos_num.cast_sub' {α : Type u_1} [add_group_with_one α] (m n : pos_num) :
↑(m.sub' n) = ↑m - ↑n
source
theorem pos_num.to_nat_eq_succ_pred (n : pos_num) :
↑n = ↑(n.pred') + 1
source
theorem pos_num.to_int_eq_succ_pred (n : pos_num) :
↑n = ↑↑(n.pred') + 1
source
@[simp]
theorem num.cast_sub' {α : Type u_1} [add_group_with_one α] (m n : num) :
↑(m.sub' n) = ↑m - ↑n
source
theorem num.to_znum_succ (n : num) :
n.succ.to_znum = n.to_znum.succ
source
theorem num.to_znum_neg_succ (n : num) :
n.succ.to_znum_neg = n.to_znum_neg.pred
source
@[simp]
theorem num.pred_succ (n : znum) :
n.pred.succ = n
source
theorem num.succ_of_int' (n : ℤ) :
znum.of_int' (n + 1) = znum.of_int' n + 1
source
theorem num.of_int'_to_znum (n : ℕ) :
↑n.to_znum = znum.of_int' ↑n
source
theorem num.mem_of_znum' {m : num} {n : znum} :
m ∈ num.of_znum' n ↔ n = m.to_znum
source
theorem num.of_znum'_to_nat (n : znum) :
coe <$> num.of_znum' n = ↑n.to_nat'
source
@[simp]
theorem num.of_znum_to_nat (n : znum) :
↑(num.of_znum n) = ↑n.to_nat
source
@[simp]
theorem num.cast_of_znum {α : Type u_1} [add_group_with_one α] (n : znum) :
↑(num.of_znum n) = ↑(↑n.to_nat)
source
@[simp, norm_cast]
theorem num.sub_to_nat (m n : num) :
↑(m - n) = ↑m - ↑n
source
@[simp, norm_cast]
theorem znum.cast_add {α : Type u_1} [add_group_with_one α] (m n : znum) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem znum.cast_succ {α : Type u_1} [add_group_with_one α] (n : znum) :
↑(n.succ) = ↑n + 1
source
@[simp, norm_cast]
theorem znum.mul_to_int (m n : znum) :
↑(m * n) = ↑m * ↑n
source
theorem znum.cast_mul {α : Type u_1} [ring α] (m n : znum) :
↑(m * n) = ↑m * ↑n
source
theorem znum.of_int'_neg (n : ℤ) :
znum.of_int' (-n) = -znum.of_int' n
source
theorem znum.of_to_int' (n : znum) :
znum.of_int' ↑n = n
source
theorem znum.to_int_inj {m n : znum} :
↑m = ↑n ↔ m = n
source
theorem znum.cmp_to_int (m n : znum) :
(m.cmp n).cases_on (↑m < ↑n) (m = n) (↑n < ↑m)
source
@[norm_cast]
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, norm_cast]
theorem znum.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
↑m < ↑n ↔ m < n
source
@[simp, norm_cast]
theorem znum.cast_le {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp, norm_cast]
theorem znum.cast_inj {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
↑m = ↑n ↔ m = n
source
meta def znum.transfer_rw  :
tactic unit

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 :=
begin
  znum.transfer_rw,
  exact le_add_of_nonneg_right (mul_self_nonneg _)
end
source
meta def znum.transfer  :
tactic unit

This tactic tries to prove (in)equalities about znums by transfering them to the int world and then trying to call simp.

example (n : znum) (m : znum) : n ≤ n + m * m :=
begin
  znum.transfer,
  exact mul_self_nonneg _
end
source
@[protected, instance]
def znum.linear_order  :
linear_order znum
Equations
source
@[protected, instance]
def znum.add_comm_group  :
add_comm_group znum
Equations
source
@[protected, instance]
def znum.add_monoid_with_one  :
add_monoid_with_one znum
Equations
source
@[protected, instance]
def znum.linear_ordered_comm_ring  :
linear_ordered_comm_ring znum
Equations
source
@[simp, norm_cast]
theorem znum.cast_sub {α : Type u_1} [ring α] (m n : znum) :
↑(m - n) = ↑m - ↑n
source
@[simp, norm_cast]
theorem znum.neg_of_int (n : ℤ) :
↑-n = -↑n
source
@[simp]
theorem znum.of_int'_eq (n : ℤ) :
znum.of_int' n = ↑n
source
@[simp]
theorem znum.of_nat_to_znum (n : ℕ) :
↑n.to_znum = ↑n
source
@[simp, norm_cast]
theorem znum.of_to_int (n : znum) :
↑↑n = n
source
theorem znum.to_of_int (n : ℤ) :
↑↑n = n
source
@[simp]
theorem znum.of_nat_to_znum_neg (n : ℕ) :
↑n.to_znum_neg = -↑n
source
@[simp, norm_cast]
theorem znum.of_int_cast {α : Type u_1} [add_group_with_one α] (n : ℤ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem znum.of_nat_cast {α : Type u_1} [add_group_with_one α] (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem znum.dvd_to_int (m n : znum) :
↑m ∣ ↑n ↔ m ∣ n
source
theorem pos_num.divmod_to_nat_aux {n d : pos_num} {q r : num} (h₁ : ↑r + ↑d * bit0 ↑q = ↑n) (h₂ : ↑r < 2 * ↑d) :
↑((d.divmod_aux q r).snd) + ↑d * ↑((d.divmod_aux q r).fst) = ↑n ∧ ↑((d.divmod_aux q r).snd) < ↑d
source
theorem pos_num.divmod_to_nat (d n : pos_num) :
↑n / ↑d = ↑((d.divmod n).fst) ∧ ↑n % ↑d = ↑((d.divmod n).snd)
source
@[simp]
theorem pos_num.div'_to_nat (n d : pos_num) :
↑(n.div' d) = ↑n / ↑d
source
@[simp]
theorem pos_num.mod'_to_nat (n d : pos_num) :
↑(n.mod' d) = ↑n % ↑d
source
@[protected, simp]
theorem num.div_zero (n : num) :
n / 0 = 0
source
@[simp, norm_cast]
theorem num.div_to_nat (n d : num) :
↑(n / d) = ↑n / ↑d
source
@[protected, simp]
theorem num.mod_zero (n : num) :
n % 0 = n
source
@[simp, norm_cast]
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).nat_size ≤ n → ↑(num.gcd_aux 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
@[protected, instance]
def num.decidable_dvd  :
decidable_rel has_dvd.dvd
Equations
source
@[protected, instance]
def pos_num.decidable_dvd  :
decidable_rel has_dvd.dvd
Equations
source
@[protected, simp]
theorem znum.div_zero (n : znum) :
n / 0 = 0
source
@[simp, norm_cast]
theorem znum.div_to_int (n d : znum) :
↑(n / d) = ↑n / ↑d
source
@[simp, norm_cast]
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
@[protected, instance]
def znum.has_dvd.dvd.decidable_rel  :
decidable_rel has_dvd.dvd
Equations
source
def int.of_snum  :
snum → ℤ

Cast a snum to the corresponding integer.

Equations
source
@[protected, instance]
def int.snum_coe  :
has_coe snum ℤ
Equations
source
@[protected, instance]
def snum.has_lt  :
has_lt snum
Equations
source
@[protected, instance]
def snum.has_le  :
has_le snum
Equations