Properties of the binary representation of integers
@[simp]
@[simp]
@[simp]
@[simp]
@[instance]
Equations
- num.comm_semiring = {add := has_add.add num.has_add, add_assoc := num.comm_semiring._proof_1, zero := 0, zero_add := num.zero_add, add_zero := num.add_zero, add_comm := num.comm_semiring._proof_2, mul := has_mul.mul num.has_mul, mul_assoc := num.comm_semiring._proof_3, one := 1, one_mul := num.comm_semiring._proof_4, mul_one := num.comm_semiring._proof_5, zero_mul := num.comm_semiring._proof_6, mul_zero := num.comm_semiring._proof_7, left_distrib := num.comm_semiring._proof_8, right_distrib := num.comm_semiring._proof_9, mul_comm := num.comm_semiring._proof_10}
@[instance]
Equations
- num.ordered_cancel_add_comm_monoid = {add := comm_semiring.add num.comm_semiring, add_assoc := _, zero := comm_semiring.zero num.comm_semiring, zero_add := _, add_zero := _, add_comm := _, add_left_cancel := num.ordered_cancel_add_comm_monoid._proof_1, add_right_cancel := num.ordered_cancel_add_comm_monoid._proof_2, le := has_le.le num.has_le, lt := has_lt.lt num.has_lt, le_refl := num.ordered_cancel_add_comm_monoid._proof_3, le_trans := num.ordered_cancel_add_comm_monoid._proof_4, lt_iff_le_not_le := num.ordered_cancel_add_comm_monoid._proof_5, le_antisymm := num.ordered_cancel_add_comm_monoid._proof_6, add_le_add_left := num.ordered_cancel_add_comm_monoid._proof_7, le_of_add_le_add_left := num.ordered_cancel_add_comm_monoid._proof_8}
@[instance]
Equations
- num.decidable_linear_ordered_semiring = {add := comm_semiring.add num.comm_semiring, add_assoc := _, zero := comm_semiring.zero num.comm_semiring, zero_add := _, add_zero := _, add_comm := _, mul := comm_semiring.mul num.comm_semiring, mul_assoc := _, one := comm_semiring.one num.comm_semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, add_right_cancel := _, le := ordered_cancel_add_comm_monoid.le num.ordered_cancel_add_comm_monoid, lt := ordered_cancel_add_comm_monoid.lt num.ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := num.decidable_linear_ordered_semiring._proof_1, mul_lt_mul_of_pos_right := num.decidable_linear_ordered_semiring._proof_2, le_total := num.decidable_linear_ordered_semiring._proof_3, zero_lt_one := num.decidable_linear_ordered_semiring._proof_4, decidable_le := num.decidable_le, decidable_eq := num.decidable_eq, decidable_lt := num.decidable_lt}
@[instance]
Equations
- pos_num.add_comm_semigroup = {add := has_add.add pos_num.has_add, add_assoc := pos_num.add_comm_semigroup._proof_1, add_comm := pos_num.add_comm_semigroup._proof_2}
@[instance]
Equations
- pos_num.comm_monoid = {mul := has_mul.mul pos_num.has_mul, mul_assoc := pos_num.comm_monoid._proof_1, one := 1, one_mul := pos_num.comm_monoid._proof_2, mul_one := pos_num.comm_monoid._proof_3, mul_comm := pos_num.comm_monoid._proof_4}
@[instance]
Equations
- pos_num.distrib = {mul := has_mul.mul pos_num.has_mul, add := has_add.add pos_num.has_add, left_distrib := pos_num.distrib._proof_1, right_distrib := pos_num.distrib._proof_2}
@[instance]
Equations
- pos_num.decidable_linear_order = {le := has_le.le pos_num.has_le, lt := has_lt.lt pos_num.has_lt, le_refl := pos_num.decidable_linear_order._proof_1, le_trans := pos_num.decidable_linear_order._proof_2, lt_iff_le_not_le := pos_num.decidable_linear_order._proof_3, le_antisymm := pos_num.decidable_linear_order._proof_4, le_total := pos_num.decidable_linear_order._proof_5, decidable_le := λ (a b : pos_num), pos_num.decidable_le a b, decidable_eq := λ (a b : pos_num), pos_num.decidable_eq a b, decidable_lt := λ (a b : pos_num), pos_num.decidable_lt a b}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
num.cast_to_znum_neg
{α : Type u_1}
[add_group α]
[has_one α]
(n : num) :
↑(n.to_znum_neg) = -↑n
@[simp]
@[simp]
@[simp]
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
@[simp]
@[simp]
@[simp]
@[instance]
Equations
- znum.decidable_linear_order = {le := has_le.le znum.has_le, lt := has_lt.lt znum.has_lt, le_refl := znum.decidable_linear_order._proof_1, le_trans := znum.decidable_linear_order._proof_2, lt_iff_le_not_le := znum.decidable_linear_order._proof_3, le_antisymm := znum.decidable_linear_order._proof_4, le_total := znum.decidable_linear_order._proof_5, decidable_le := znum.decidable_le, decidable_eq := znum.decidable_eq, decidable_lt := znum.decidable_lt}
@[instance]
Equations
- znum.add_comm_group = {add := has_add.add znum.has_add, add_assoc := znum.add_comm_group._proof_1, zero := 0, zero_add := znum.zero_add, add_zero := znum.add_zero, neg := has_neg.neg znum.has_neg, add_left_neg := znum.add_comm_group._proof_2, add_comm := znum.add_comm_group._proof_3}
@[instance]
Equations
- znum.decidable_linear_ordered_comm_ring = {add := add_comm_group.add znum.add_comm_group, add_assoc := _, zero := add_comm_group.zero znum.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg znum.add_comm_group, add_left_neg := _, add_comm := _, mul := has_mul.mul znum.has_mul, mul_assoc := znum.decidable_linear_ordered_comm_ring._proof_1, one := 1, one_mul := znum.decidable_linear_ordered_comm_ring._proof_2, mul_one := znum.decidable_linear_ordered_comm_ring._proof_3, left_distrib := znum.decidable_linear_ordered_comm_ring._proof_4, right_distrib := znum.decidable_linear_ordered_comm_ring._proof_5, le := decidable_linear_order.le znum.decidable_linear_order, lt := decidable_linear_order.lt znum.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := znum.decidable_linear_ordered_comm_ring._proof_6, exists_pair_ne := znum.decidable_linear_ordered_comm_ring._proof_7, mul_pos := znum.decidable_linear_ordered_comm_ring._proof_8, le_total := _, zero_lt_one := znum.decidable_linear_ordered_comm_ring._proof_9, mul_comm := znum.decidable_linear_ordered_comm_ring._proof_10, decidable_le := decidable_linear_order.decidable_le znum.decidable_linear_order, decidable_eq := decidable_linear_order.decidable_eq znum.decidable_linear_order, decidable_lt := decidable_linear_order.decidable_lt znum.decidable_linear_order}
@[instance]
Equations
- num.decidable_dvd a b = decidable_of_iff' (b % a = 0) num.dvd_iff_mod_eq_zero
@[instance]
Equations
- pos_num.decidable_dvd a b = num.decidable_dvd (num.pos a) (num.pos b)
@[instance]
Equations
- znum.decidable_rel a b = decidable_of_iff' (b % a = 0) znum.dvd_iff_mod_eq_zero