feat(data/zmod/quadratic_reciprocity): quadratic reciprocity (#327)

* multiplicative group of finite field is cyclic

* more stuff

* change chinese remainder to def

* get rid of nonsense

* delete extra line break

* one prod_bij left

* move lemmas to correct places

* delete prod_instances

* almost done

* move lamms to correct places

* more moving lemmas

* finished off moving lemmas

* fix build

* move quadratic reciprocity to zmod

* improve readability

* remove unnecessary alphas

* move `prod_range_id`

* fix build

* fix build

* fix build

* fix build

* delete mk_of_ne_zero

* move odd_mul_odd_div_two

* extra a few lemmas

* improving readability

* delete duplicate lemmas

* forgot to save

* delete duplicate lemma

* indent calc proofs

* fix build

* fix build

* forgot to save

* fix build

algebra/big_operators.lean

@@ -54,7 +54,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
 
@@ -229,14 +229,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 : ℕ → β) :
@@ -257,6 +313,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
@@ -402,6 +475,17 @@ end discrete_linear_ordered_field
   (s.pi t).card = s.prod (λ a, card (t a)) :=
 multiset.card_pi _ _
 
+@[simp] lemma prod_range_id_eq_fact (n : ℕ) : ((range n.succ).erase 0).prod (λ x, x) = nat.fact n :=
+calc ((range n.succ).erase 0).prod (λ x, x) = (range n).prod nat.succ :
+eq.symm (prod_bij (λ x _, nat.succ x)
+  (λ a h₁, mem_erase.2 ⟨nat.succ_ne_zero _, mem_range.2 $ nat.succ_lt_succ $ by simpa using h₁⟩)
+  (by simp) (λ _ _ _ _, nat.succ_inj)
+  (λ b h,
+    have b.pred.succ = b, from nat.succ_pred_eq_of_pos $
+      by simp [nat.pos_iff_ne_zero] at *; tauto,
+    ⟨nat.pred b, mem_range.2 $ nat.lt_of_succ_lt_succ (by simp [*, - range_succ] at *), this.symm⟩))
+... = nat.fact n : by induction n; simp *
+
 end finset
 
 section group

algebra/field.lean

@@ -32,6 +32,10 @@ def mk0 (a : α) (ha : a ≠ 0) : units α :=
 
 @[simp] theorem mk0_inv (ha : a ≠ 0) : ((mk0 a ha)⁻¹ : α) = a⁻¹ := rfl
 
+@[simp] lemma units.mk0_inj [field α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
+  units.mk0 a ha = units.mk0 b hb ↔ a = b :=
+⟨λ h, by injection h, λ h, units.ext h⟩
+
 end units
 
 section division_ring

algebra/field_power.lean

@@ -42,7 +42,7 @@ lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z
 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
+begin simp only [fpow_eq_gpow ha], rw ← units.coe_mul, congr, apply gpow_add end
 
 end field_power
 

algebra/group.lean

@@ -226,10 +226,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 _
 

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 : ℕ) :
@@ -366,6 +369,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_pow_mod_two [ring α] {n : ℕ} : (-1 : α) ^ n = -1 ^ (n % 2) :=
+by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
+
 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)
+
 lemma mul_le_one {a b : α} (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1 :=
 begin rw ← one_mul (1 : α), apply mul_le_mul; {assumption <|> apply zero_le_one} end
 

algebra/pi_instances.lean

@@ -224,4 +224,14 @@ instance {r : ring α} [module α β] [module α γ] : module α (β × γ) :=
 
 instance {r : field α} [vector_space α β] [vector_space α γ] : vector_space α (β × γ) := {}
 
-end prod
+end prod
+
+namespace finset
+
+@[to_additive finset.prod_mk_sum]
+lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : finset γ)
+  (f : γ → α) (g : γ → β) : (s.prod f, s.prod g) = s.prod (λ x, (f x, g x)) :=
+by haveI := classical.dec_eq γ; exact
+finset.induction_on s rfl (by simp [prod.ext_iff] {contextual := tt})
+
+end finset

algebra/ring.lean

@@ -191,6 +191,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. -/
@@ -256,6 +259,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/finset.lean

@@ -853,9 +853,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 :=
@@ -926,6 +926,44 @@ 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 _ _
+
+lemma surj_on_of_inj_on_of_card_le {s : finset α} {t : finset β}
+  (f : Π a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t)
+  (hinj : ∀ a₁ a₂ ha₁ ha₂, f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂)
+  (hst : card t ≤ card s) :
+  (∀ b ∈ t, ∃ a ha, b = f a ha) :=
+by haveI := classical.dec_eq β; exact
+λ b hb,
+  have h : card (image (λ (a : {a // a ∈ s}), f (a.val) a.2) (attach s)) = card s,
+    from @card_attach _ s ▸ card_image_of_injective _
+      (λ ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h, subtype.eq $ hinj _ _ _ _ h),
+  have h₁ : image (λ a : {a // a ∈ s}, f a.1 a.2) s.attach = t :=
+  eq_of_subset_of_card_le (λ b h, let ⟨a, ha₁, ha₂⟩ := mem_image.1 h in
+    ha₂ ▸ hf _ _) (by simp [hst, h]),
+begin
+  rw ← h₁ at hb,
+  rcases mem_image.1 hb with ⟨a, ha₁, ha₂⟩,
+  exact ⟨a, a.2, ha₂.symm⟩,
+end
+
 end card
 
 section bind
@@ -1124,7 +1162,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]
 

data/int/modeq.lean

@@ -56,6 +56,8 @@ modeq_iff_dvd.2 $ by rwa add_neg_cancel_left at this
 theorem modeq_add_cancel_right (h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) : a ≡ b [ZMOD n] :=
 by rw [add_comm a, add_comm b] at h₂; exact modeq_add_cancel_left h₁ h₂
 
+theorem mod_modeq (a n) : a % n ≡ a [ZMOD n] := int.mod_mod _ _
+
 theorem modeq_neg (h : a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n] :=
 modeq_add_cancel_left h (by simp)
 
@@ -75,5 +77,33 @@ by rw [mul_comm a, mul_comm b]; exact modeq_mul_left c h
 theorem modeq_mul (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] :=
 (modeq_mul_left _ h₂).trans (modeq_mul_right _ h₁)
 
+theorem modeq_of_modeq_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] :=
+by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left n m) h
+
+theorem modeq_of_modeq_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
+mul_comm m n ▸ modeq_of_modeq_mul_left _
+
+lemma modeq_and_modeq_iff_modeq_mul {a b m n : ℤ} (hmn : nat.coprime m.nat_abs n.nat_abs) :
+  a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ (a ≡ b [ZMOD m * n]) :=
+⟨λ h, begin
+    rw [int.modeq.modeq_iff_dvd, int.modeq.modeq_iff_dvd] at h,
+    rw [int.modeq.modeq_iff_dvd, ← int.nat_abs_dvd, ← int.dvd_nat_abs,
+      int.coe_nat_dvd, int.nat_abs_mul],
+    refine hmn.mul_dvd_of_dvd_of_dvd _ _;
+    rw [← int.coe_nat_dvd, int.nat_abs_dvd, int.dvd_nat_abs]; tauto
+  end,
+λ h, ⟨int.modeq.modeq_of_modeq_mul_right _ h, int.modeq.modeq_of_modeq_mul_left _ h⟩⟩
+
+lemma gcd_a_modeq (a b : ℕ) : (a : ℤ) * nat.gcd_a a b ≡ nat.gcd a b [ZMOD b] :=
+by rw [← add_zero ((a : ℤ) * _), nat.gcd_eq_gcd_ab];
+  exact int.modeq.modeq_add rfl (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _)).symm
+
 end modeq
+
+@[simp] lemma mod_mul_right_mod (a b c : ℤ) : a % (b * c) % b = a % b :=
+int.modeq.modeq_of_modeq_mul_right _ (int.modeq.mod_modeq _ _)
+
+@[simp] lemma mod_mul_left_mod (a b c : ℤ) : a % (b * c) % c = a % c :=
+int.modeq.modeq_of_modeq_mul_left _ (int.modeq.mod_modeq _ _)
+
 end int