feat(data/num,data/multiset): more properties of binary numbers, begi…

…n multisets

algebra/field.lean

@@ -12,6 +12,18 @@ variables {α : Type u}
 section division_ring
 variables [division_ring α] {a b : α}
 
+lemma inv_ne_zero {a : α} (h : a ≠ 0) : a⁻¹ ≠ 0 :=
+by rw inv_eq_one_div; exact one_div_ne_zero h
+
+@[simp] lemma division_ring.inv_inv {a : α} (h : a ≠ 0) : a⁻¹⁻¹ = a :=
+by rw [inv_eq_one_div, inv_eq_one_div, division_ring.one_div_one_div h]
+
+lemma division_ring.inv_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (a / b)⁻¹ = b / a :=
+by rw [division_def, mul_inv_eq (inv_ne_zero hb) ha, division_ring.inv_inv hb, division_def]
+
+lemma division_ring.one_div_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / (a / b) = b / a :=
+by rw [one_div_eq_inv, division_ring.inv_div ha hb]
+
 lemma division_ring.neg_inv (h : a ≠ 0) : - a⁻¹ = (- a)⁻¹ :=
 by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
 

algebra/group_power.lean

@@ -27,6 +27,9 @@ class has_pow_nat (α : Type u) :=
 def pow_nat {α : Type u} [has_pow_nat α] : α → nat → α :=
 has_pow_nat.pow_nat
 
+@[simp] theorem has_pow_nat_eq_pow_nat {α : Type u} [has_pow_nat α] :
+  @has_pow_nat.pow_nat α _ = pow_nat := rfl
+
 infix ` ^ ` := pow_nat
 
 class has_pow_int (α : Type u) :=
@@ -68,6 +71,10 @@ theorem pow_mul (a : α) (m : ℕ) : ∀ n, a^(m * n) = (a^m)^n
 | 0     := by simp
 | (n+1) := by rw [nat.mul_succ, pow_add, pow_succ', pow_mul]
 
+theorem pow_bit0 (a : α) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
+theorem pow_bit1 (a : α) (n : ℕ) : a ^ bit1 n = a^n * a^n * a :=
+by rw [bit1, pow_succ', pow_bit0]
+
 theorem pow_mul_comm (a : α) (m n : ℕ)  : a^m * a^n = a^n * a^m :=
 by rw [←pow_add, ←pow_add, add_comm]
 

algebra/ordered_group.lean

@@ -44,6 +44,9 @@ by split; apply le_antisymm; try {assumption};
    rw ← hab; simp [ha, hb],
 λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩
 
+lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
+add_pos h h
+
 end ordered_cancel_comm_monoid
 
 section ordered_comm_group

algebra/ordered_ring.lean

@@ -53,6 +53,12 @@ mul_le_mul_of_nonneg_right h hb
 theorem mul_nonneg_iff_right_nonneg_of_pos {a b : α} (h : 0 < a) : 0 ≤ b * a ↔ 0 ≤ b :=
 ⟨assume : 0 ≤ b * a, nonneg_of_mul_nonneg_right this h, assume : 0 ≤ b, mul_nonneg this $ le_of_lt h⟩
 
+lemma bit1_pos {a : α} (h : 0 ≤ a) : 0 < bit1 a :=
+lt_add_of_le_of_pos (add_nonneg h h) zero_lt_one
+
+lemma bit1_pos' {a : α} (h : 0 < a) : 0 < bit1 a :=
+bit1_pos (le_of_lt h)
+
 /- remove when we have a linear arithmetic tactic -/
 lemma one_lt_two : 1 < (2 : α) :=
 calc (1:α) < 1 + 1 : lt_add_of_le_of_pos (le_refl 1) zero_lt_one

data/int/basic.lean

@@ -822,6 +822,9 @@ protected def cast : ℤ → α
 
 @[simp] theorem cast_of_nat (n : ℕ) : (of_nat n : α) = n := rfl
 @[simp] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n := rfl
+@[simp] theorem cast_coe_nat' (n : ℕ) :
+  (@coe ℕ ℤ (@coe_to_lift _ _ (@coe_base _ _ nat.cast_coe)) n : α) = n :=
+by simp
 
 @[simp] theorem cast_neg_succ_of_nat (n : ℕ) : (-[1+ n] : α) = -(n + 1) := rfl