@[instance]
Equations
- int.comm_ring = {add := int.add, add_assoc := int.add_assoc, zero := int.zero, zero_add := int.zero_add, add_zero := int.add_zero, neg := int.neg, sub := int.sub, sub_eq_add_neg := int.comm_ring._proof_1, add_left_neg := int.add_left_neg, add_comm := int.add_comm, mul := int.mul, mul_assoc := int.mul_assoc, one := int.one, one_mul := int.one_mul, mul_one := int.mul_one, left_distrib := int.distrib_left, right_distrib := int.distrib_right, mul_comm := int.mul_comm}
Extra instances to short-circuit type class resolution
@[instance]
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
- int.linear_ordered_comm_ring = {add := comm_ring.add int.comm_ring, add_assoc := _, zero := comm_ring.zero int.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg int.comm_ring, sub := comm_ring.sub int.comm_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul int.comm_ring, mul_assoc := _, one := comm_ring.one int.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_order.le int.linear_order, lt := linear_order.lt int.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := int.add_le_add_left, zero_le_one := int.linear_ordered_comm_ring._proof_1, mul_pos := int.mul_pos, le_total := _, decidable_le := linear_order.decidable_le int.linear_order, decidable_eq := linear_order.decidable_eq int.linear_order, decidable_lt := linear_order.decidable_lt int.linear_order, exists_pair_ne := _, mul_comm := _}
succ and pred
Inductively define a function on ℤ
by defining it at b
, for the succ
of a number greater
than b
, and the pred
of a number less than b
.
Equations
- z.induction_on' b = λ (H0 : C b) (Hs : Π (k : ℤ), b ≤ k → C k → C (k + 1)) (Hp : Π (k : ℤ), k ≤ b → C k → C (k - 1)), _.mpr (int.rec (λ (n : ℕ), nat.rec (_.mpr (_.mpr H0)) (λ (n : ℕ) (ih : C (int.of_nat n + b)), _.mpr (_.mpr (_.mpr (_.mpr (Hs (int.of_nat n + b) _ ih))))) n) (λ (n : ℕ), nat.rec (_.mpr (_.mpr (_.mpr (_.mpr (_.mpr (Hp b _ H0)))))) (λ (n : ℕ) (ih : C (-[1+ n] + b)), _.mpr (_.mpr (_.mpr (_.mpr (Hp (-[1+ n] + b) _ ih))))) n) (z - b))
nat abs
/
mod
properties of /
and %
dvd
@[instance]
Equations
- int.decidable_dvd = λ (a n : ℤ), decidable_of_decidable_of_iff (int.decidable_eq (n % a) 0) _
/
and ordering
theorem
int.of_nat_add_neg_succ_of_nat_of_ge
{m n : ℕ}
(h : n.succ ≤ m) :
int.of_nat m + -[1+ n] = int.of_nat (m - n.succ)
to_nat
units
bitwise ops
@[simp]
@[simp]
theorem
int.bitwise_bit
(f : bool → bool → bool)
(a : bool)
(m : ℤ)
(b : bool)
(n : ℤ) :
int.bitwise f (int.bit a m) (int.bit b n) = int.bit (f a b) (int.bitwise f m n)