feat(data/zmod/quadratic_reciprocity): quadratic reciprocity

algebra/big_operators.lean

@@ -42,7 +42,7 @@ by simp [finset.prod]
 attribute [to_additive finset.sum_const_zero] prod_const_one
 
 @[simp, to_additive finset.sum_image]
-lemma prod_image [decidable_eq α] [decidable_eq γ] {s : finset γ} {g : γ → α} :
+lemma prod_image [decidable_eq α] {s : finset γ} {g : γ → α} :
   (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) :=
 fold_image
 
@@ -217,14 +217,70 @@ lemma prod_range_succ' (f : ℕ → β) :
 | (n + 1) := by rw [prod_range_succ (λ m, f (nat.succ m)), mul_assoc, ← prod_range_succ'];
                  exact prod_range_succ _ _
 
-@[simp] lemma prod_const [decidable_eq α] (b : β) : s.prod (λ a, b) = b ^ s.card :=
+@[simp] lemma prod_const (b : β) : s.prod (λ a, b) = b ^ s.card :=
+by haveI := classical.dec_eq α; exact
 finset.induction_on s rfl (by simp [pow_add, mul_comm] {contextual := tt})
 
+lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
+  s.prod (λ x, f x ^ n) = s.prod f ^ n :=
+by haveI := classical.dec_eq α; exact
+finset.induction_on s (by simp) (by simp [_root_.mul_pow] {contextual := tt})
+
+lemma prod_nat_pow (s : finset α) (n : ℕ) (f : α → ℕ) :
+  s.prod (λ x, f x ^ n) = s.prod f ^ n :=
+by haveI := classical.dec_eq α; exact
+finset.induction_on s (by simp) (by simp [nat.mul_pow] {contextual := tt})
+
+@[to_additive finset.sum_involution]
+lemma prod_involution {s : finset α} {f : α → β} :
+  ∀ (g : Π a ∈ s, α)
+  (h₁ : ∀ a ha, f a * f (g a ha) = 1)
+  (h₂ : ∀ a ha, f a ≠ 1 → g a ha ≠ a)
+  (h₃ : ∀ a ha, g a ha ∈ s)
+  (h₄ : ∀ a ha, g (g a ha) (h₃ a ha) = a),
+  s.prod f = 1 :=
+by haveI := classical.dec_eq α;
+haveI := classical.dec_eq β; exact
+finset.strong_induction_on s
+  (λ s ih g h₁ h₂ h₃ h₄,
+    if hs : s = ∅ then hs.symm ▸ rfl
+    else let ⟨x, hx⟩ := exists_mem_of_ne_empty hs in
+      have hmem : ∀ y ∈ (s.erase x).erase (g x hx), y ∈ s,
+        from λ y hy, (mem_of_mem_erase (mem_of_mem_erase hy)),
+      have g_inj : ∀ {x hx y hy}, g x hx = g y hy → x = y,
+        from λ x hx y hy h, by rw [← h₄ x hx, ← h₄ y hy]; simp [h],
+      have ih': (erase (erase s x) (g x hx)).prod f = (1 : β) :=
+        ih ((s.erase x).erase (g x hx))
+          ⟨subset.trans (erase_subset _ _) (erase_subset _ _),
+            λ h, not_mem_erase (g x hx) (s.erase x) (h (h₃ x hx))⟩
+          (λ y hy, g y (hmem y hy))
+          (λ y hy, h₁ y (hmem y hy))
+          (λ y hy, h₂ y (hmem y hy))
+          (λ y hy, mem_erase.2 ⟨λ (h : g y _ = g x hx), by simpa [g_inj h] using hy,
+            mem_erase.2 ⟨λ (h : g y _ = x),
+              have y = g x hx, from h₄ y (hmem y hy) ▸ by simp [h],
+              by simpa [this] using hy, h₃ y (hmem y hy)⟩⟩)
+          (λ y hy, h₄ y (hmem y hy)),
+      if hx1 : f x = 1
+      then ih' ▸ eq.symm (prod_subset hmem
+        (λ y hy hy₁,
+          have y = x ∨ y = g x hx, by simp [hy] at hy₁; tauto,
+          this.elim (λ h, h.symm ▸ hx1)
+            (λ h, h₁ x hx ▸ h ▸ hx1.symm ▸ (one_mul _).symm)))
+      else by rw [← insert_erase hx, prod_insert (not_mem_erase _ _),
+        ← insert_erase (mem_erase.2 ⟨h₂ x hx hx1, h₃ x hx⟩),
+        prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx])
+
 end comm_monoid
 
-@[simp] lemma sum_const [add_comm_monoid β] [decidable_eq α] (b : β) :
+lemma sum_smul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
+  s.sum (λ x, add_monoid.smul n (f x)) = add_monoid.smul n (s.sum f) :=
+@prod_pow _ (multiplicative β) _ _ _ _
+attribute [to_additive finset.sum_smul] prod_pow
+
+@[simp] lemma sum_const [add_comm_monoid β] (b : β) :
   s.sum (λ a, b) = add_monoid.smul s.card b :=
-@prod_const _ (multiplicative β) _ _ _ _
+@prod_const _ (multiplicative β) _ _ _
 attribute [to_additive finset.sum_const] prod_const
 
 lemma sum_range_succ' [add_comm_monoid β] (f : ℕ → β) :
@@ -245,6 +301,23 @@ end comm_group
   card (s.sigma t) = s.sum (λ a, card (t a)) :=
 multiset.card_sigma _ _
 
+lemma card_bind [decidable_eq β] {s : finset α} {t : α → finset β}
+  (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → t x ∩ t y = ∅) :
+  (s.bind t).card = s.sum (λ u, card (t u)) :=
+calc (s.bind t).card = (s.bind t).sum (λ _, 1) : by simp
+... = s.sum (λ a, (t a).sum (λ _, 1)) : finset.sum_bind h
+... = s.sum (λ u, card (t u)) : by simp
+
+lemma card_bind_le [decidable_eq β] {s : finset α} {t : α → finset β} :
+  (s.bind t).card ≤ s.sum (λ a, (t a).card) :=
+by haveI := classical.dec_eq α; exact
+finset.induction_on s (by simp)
+  (λ a s has ih,
+    calc ((insert a s).bind t).card ≤ (t a).card + (s.bind t).card :
+    by rw bind_insert; exact finset.card_union_le _ _
+    ... ≤ (insert a s).sum (λ a, card (t a)) :
+    by rw sum_insert has; exact add_le_add_left ih _)
+
 end finset
 
 namespace finset

algebra/field_power.lean

@@ -11,57 +11,57 @@ import algebra.group_power tactic.wlog
 universe u
 
 section field_power
-open int nat 
+open int nat
 variables {α : Type u} [division_ring α]
 
 @[simp] lemma zero_gpow : ∀ z : ℕ, z ≠ 0 → (0 : α)^z = 0
-| 0 h := absurd rfl h 
-| (k+1) h := zero_mul _ 
+| 0 h := absurd rfl h
+| (k+1) h := zero_mul _
 
-def fpow (a : α) : ℤ → α 
-| (of_nat n) := a ^ n 
+def fpow (a : α) : ℤ → α
+| (of_nat n) := a ^ n
 | -[1+n] := 1/(a ^ (n+1))
 
 lemma unit_pow {a : α} (ha : a ≠ 0) : ∀ n : ℕ, a ^ n = ↑((units.mk0 a ha)^n)
 | 0 := by simp; refl
-| (k+1) := by simp [_root_.pow_add]; congr; apply unit_pow 
+| (k+1) := by simp [_root_.pow_add]; congr; apply unit_pow
 
 lemma fpow_eq_gpow {a : α} (h : a ≠ 0) : ∀ (z : ℤ), fpow a z = ↑(gpow (units.mk0 a h) z)
-| (of_nat k) := by simp only [fpow, gpow]; apply unit_pow 
-| -[1+k] := by simp [fpow, gpow]; congr; apply unit_pow 
+| (of_nat k) := by simp only [fpow, gpow]; apply unit_pow
+| -[1+k] := by simp [fpow, gpow]; congr; apply unit_pow
 
-lemma fpow_inv (a : α) : fpow a (-1) = a⁻¹ := 
-begin change fpow a -[1+0] = a⁻¹, simp [fpow] end 
+lemma fpow_inv (a : α) : fpow a (-1) = a⁻¹ :=
+begin change fpow a -[1+0] = a⁻¹, simp [fpow] end
 
 lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z ≠ 0
 | (of_nat n) := pow_ne_zero _ ha
 | -[1+n] := one_div_ne_zero $ pow_ne_zero _ ha
 
 
 @[simp] lemma fpow_zero {a : α} : fpow a 0 = 1 :=
-pow_zero _ 
+pow_zero _
 
-lemma fpow_add {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 + z2) = fpow a z1 * fpow a z2 := 
-begin simp only [fpow_eq_gpow ha], rw ←units.mul_coe, congr, apply gpow_add end 
+lemma fpow_add {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 + z2) = fpow a z1 * fpow a z2 :=
+begin simp only [fpow_eq_gpow ha], rw ← units.coe_mul, congr, apply gpow_add end
 
 end field_power
 
 section discrete_field_power
-open int nat 
+open int nat
 variables {α : Type u} [discrete_field α]
 
 lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → fpow (0 : α) z = 0
 | (of_nat n) h :=
   have h2 : n ≠ 0, from assume : n = 0, by simpa [this] using h,
   by simp [h, h2, fpow]
-| -[1+n] h := 
+| -[1+n] h :=
   have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
   by simp [fpow, h1]
 
 end discrete_field_power
 
 section ordered_field_power
-open int 
+open int
 
 variables {α : Type u} [discrete_linear_ordered_field α]
 
@@ -71,15 +71,15 @@ lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), fpow a z 
 
 
 lemma fpow_le_of_le {x : α} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : fpow x a ≤ fpow x b :=
-begin 
+begin
   induction a with a a; induction b with b b,
-  { simp only [fpow], 
-    apply pow_le_pow hx, 
+  { simp only [fpow],
+    apply pow_le_pow hx,
     apply le_of_coe_nat_le_coe_nat h },
-  { apply absurd h, 
+  { apply absurd h,
     apply not_le_of_gt,
     exact lt_of_lt_of_le (neg_succ_lt_zero _) (of_nat_nonneg _) },
-  { simp only [fpow, one_div_eq_inv], 
+  { simp only [fpow, one_div_eq_inv],
     apply le_trans (inv_le_one _); apply one_le_pow_of_one_le hx },
   { simp only [fpow],
     apply (one_div_le_one_div _ _).2,
@@ -90,16 +90,16 @@ begin
     repeat { apply pow_pos (lt_of_lt_of_le zero_lt_one hx) } }
 end
 
-lemma pow_le_max_of_min_le {x : α} (hx : x ≥ 1) {a b c : ℤ} (h : min a b ≤ c) : 
+lemma pow_le_max_of_min_le {x : α} (hx : x ≥ 1) {a b c : ℤ} (h : min a b ≤ c) :
       fpow x (-c) ≤ max (fpow x (-a)) (fpow x (-b)) :=
-begin 
+begin
   wlog hle : a ≤ b,
   have hnle : -b ≤ -a, from neg_le_neg hle,
   have hfle : fpow x (-b) ≤ fpow x (-a), from fpow_le_of_le hx hnle,
-  have : fpow x (-c) ≤ fpow x (-a), 
+  have : fpow x (-c) ≤ fpow x (-a),
   { apply fpow_le_of_le hx,
     simpa [hle, min_eq_left] using h },
-  simpa [hfle, max_eq_left] using this 
-end 
+  simpa [hfle, max_eq_left] using this
+end
 
-end ordered_field_power 
+end ordered_field_power

algebra/group.lean

@@ -225,10 +225,10 @@ instance : has_one (units α) := ⟨⟨1, 1, mul_one 1, one_mul 1⟩⟩
 instance : has_inv (units α) := ⟨units.inv'⟩
 
 variables (a b)
-@[simp] lemma mul_coe : (↑(a * b) : α) = a * b := rfl
-@[simp] lemma one_coe : ((1 : units α) : α) = 1 := rfl
+@[simp] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
+@[simp] lemma coe_one : ((1 : units α) : α) = 1 := rfl
 lemma val_coe : (↑a : α) = a.val := rfl
-lemma inv_coe : ((a⁻¹ : units α) : α) = a.inv := rfl
+lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl
 @[simp] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
 @[simp] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _
 
@@ -274,6 +274,16 @@ end
 def units.mk_of_mul_eq_one [comm_monoid α] (a b : α) (hab : a * b = 1) : units α :=
 ⟨a, b, hab, by rwa mul_comm a b at hab⟩
 
+def units.mk_of_ne_zero [field α] {a : α} (ha : a ≠ 0) : units α :=
+⟨a, a⁻¹, mul_inv_cancel ha, inv_mul_cancel ha⟩
+
+@[simp] lemma units.mk_of_ne_zero_inj {α : Type*} [field α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
+  units.mk_of_ne_zero ha = units.mk_of_ne_zero hb ↔ a = b :=
+⟨λ h, by injection h, λ h, units.ext h⟩
+
+@[simp] lemma units.coe_mk_of_ne_zero {α : Type*} [field α] {a : α} (ha : a ≠ 0) :
+  (units.mk_of_ne_zero ha : α) = a := rfl
+
 @[to_additive with_zero]
 def with_one (α) := option α
 

algebra/group_power.lean

@@ -118,6 +118,9 @@ attribute [to_additive smul_add_comm] pow_mul_comm
 @list.prod_repeat (multiplicative β) _
 attribute [to_additive list.sum_repeat] list.prod_repeat
 
+@[simp] lemma units.coe_pow (u : units α) (n : ℕ) : ((u ^ n : units α) : α) = u ^ n :=
+by induction n; simp [*, pow_succ]
+
 end monoid
 
 @[simp] theorem nat.pow_eq_pow (p q : ℕ) :
@@ -329,6 +332,9 @@ theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
   (f : α → β) [is_semiring_hom f] (x : α) (n : ℕ) : f (x ^ n) = f x ^ n :=
 by induction n; simp [*, is_semiring_hom.map_one f, is_semiring_hom.map_mul f, pow_succ]
 
+lemma zero_pow [semiring α] {n : ℕ} : 0 < n → (0 : α) ^ n = 0 :=
+by cases n; simp [_root_.pow_succ, lt_irrefl]
+
 theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
 | 0     := by simp
 | (n+1) := by cases neg_one_pow_eq_or n; simp [pow_succ, h]
@@ -349,6 +355,9 @@ by rw [gsmul_eq_mul, gsmul_eq_mul, mul_assoc]
 @[simp] theorem int.cast_pow [ring α] (n : ℤ) (m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=
 by induction m; simp [*, nat.succ_eq_add_one,pow_add]
 
+lemma neg_one_pow_eq_one_or_neg_one [ring α] (n : ℕ) : (-1 : α) ^ n = 1 ∨ (-1 : α) ^ n = -1 :=
+by induction n; finish [_root_.pow_succ]
+
 theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 by induction n with n ih; simp [pow_succ, mul_eq_zero, *]
 

algebra/ordered_ring.lean

@@ -75,6 +75,9 @@ lt_add_of_le_of_pos (le_refl _) zero_lt_one
 
 lemma one_lt_two : 1 < (2 : α) := lt_add_one _
 
+lemma one_lt_mul {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
+(one_mul (1 : α)) ▸ mul_lt_mul' ha hb zero_le_one (lt_of_lt_of_le zero_lt_one ha)
+
 end linear_ordered_semiring
 
 instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_semiring α] :

algebra/ring.lean

@@ -176,6 +176,9 @@ instance integral_domain.to_nonzero_comm_ring (α : Type*) [id : integral_domain
   nonzero_comm_ring α :=
 { ..id }
 
+lemma units.coe_ne_zero [nonzero_comm_ring α] (u : units α) : (u : α) ≠ 0 :=
+λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3
+
 /-- A domain is a ring with no zero divisors, i.e. satisfying
   the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
   is an integral domain without assuming commutativity of multiplication. -/
@@ -241,6 +244,10 @@ section
   theorem mul_dvd_mul_iff_right {a b c : α} (hc : c ≠ 0) : a * c ∣ b * c ↔ a ∣ b :=
   exists_congr $ λ d, by rw [mul_right_comm, domain.mul_right_inj hc]
 
+  lemma units.inv_eq_self_iff (u : units α) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
+  by conv {to_lhs, rw [inv_eq_iff_mul_eq_one, ← mul_one (1 : units α), units.ext_iff, units.coe_mul,
+    units.coe_mul, mul_self_eq_mul_self_iff, ← units.ext_iff, ← units.coe_neg, ← units.ext_iff] }
+
 end
 
 /- units in various rings -/

data/equiv/basic.lean

@@ -582,16 +582,16 @@ eq_of_to_fun_eq $ funext $ λ r, swap_core_comm r _ _
 theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
 rfl
 
-theorem swap_apply_left (a b : α) : swap a b a = b :=
+@[simp] theorem swap_apply_left (a b : α) : swap a b a = b :=
 if_pos rfl
 
-theorem swap_apply_right (a b : α) : swap a b b = a :=
+@[simp] theorem swap_apply_right (a b : α) : swap a b b = a :=
 by by_cases b = a; simp [swap_apply_def, *]
 
 theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x = x :=
 by simp [swap_apply_def] {contextual := tt}
 
-theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
+@[simp] theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
 eq_of_to_fun_eq $ funext $ λ x, swap_core_swap_core _ _ _
 
 theorem swap_comp_apply {a b x : α} (π : perm α) :

data/finset.lean

@@ -851,9 +851,9 @@ by by_cases a ∈ s; simp [h, nat.le_add_right]
 
 theorem card_erase_of_mem [decidable_eq α] {a : α} {s : finset α} : a ∈ s → card (erase s a) = pred (card s) := card_erase_of_mem
 
-theorem card_range (n : ℕ) : card (range n) = n := card_range n
+@[simp] theorem card_range (n : ℕ) : card (range n) = n := card_range n
 
-theorem card_attach {s : finset α} : card (attach s) = card s := multiset.card_attach
+@[simp] theorem card_attach {s : finset α} : card (attach s) = card s := multiset.card_attach
 
 theorem card_image_of_inj_on [decidable_eq β] {f : α → β} {s : finset α}
   (H : ∀x∈s, ∀y∈s, f x = f y → x = y) : card (image f s) = card s :=
@@ -924,6 +924,25 @@ finset.strong_induction_on s $ λ s,
 finset.induction_on s (λ _, h₀) $ λ a s n _ ih, h₁ a s n $
 λ t ss, ih _ (lt_of_le_of_lt ss (ssubset_insert n) : t < _)
 
+lemma card_congr {s : finset α} {t : finset β} (f : Π a ∈ s, β)
+  (h₁ : ∀ a ha, f a ha ∈ t) (h₂ : ∀ a b ha hb, f a ha = f b hb → a = b)
+  (h₃ : ∀ b ∈ t, ∃ a ha, f a ha = b) : s.card = t.card :=
+by haveI := classical.prop_decidable; exact
+calc s.card = s.attach.card : card_attach.symm
+... = (s.attach.image (λ (a : {a // a ∈ s}), f a.1 a.2)).card :
+  eq.symm (card_image_of_injective _ (λ a b h, subtype.eq (h₂ _ _ _ _ h)))
+... = t.card : congr_arg card (finset.ext.2 $ λ b,
+    ⟨λ h, let ⟨a, ha₁, ha₂⟩ := mem_image.1 h in ha₂ ▸ h₁ _ _,
+      λ h, let ⟨a, ha₁, ha₂⟩ := h₃ b h in mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
+
+lemma card_union_add_card_inter [decidable_eq α] (s t : finset α) :
+  (s ∪ t).card + (s ∩ t).card = s.card + t.card :=
+finset.induction_on t (by simp) (λ a, by by_cases a ∈ s; simp * {contextual := tt})
+
+lemma card_union_le [decidable_eq α] (s t : finset α) :
+  (s ∪ t).card ≤ s.card + t.card :=
+card_union_add_card_inter s t ▸ le_add_right _ _
+
 end card
 
 section bind
@@ -1122,7 +1141,7 @@ by simp [fold, ndinsert_of_not_mem h]
 @[simp] theorem fold_singleton : (singleton a).fold op b f = f a * b :=
 by simp [fold]
 
-@[simp] theorem fold_image [decidable_eq α] [decidable_eq γ] {g : γ → α} {s : finset γ}
+@[simp] theorem fold_image [decidable_eq α] {g : γ → α} {s : finset γ}
   (H : ∀ (x ∈ s) (y ∈ s), g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g) :=
 by simp [fold, image_val_of_inj_on H, map_map]