feat(data/polynomial): lemmas relating unit and irreducible with degree (#514)

Author: ChrisHughes24

algebra/ordered_group.lean

@@ -336,6 +336,8 @@ end
 
 instance has_one [has_one α] : has_one (with_bot α) := ⟨(1 : α)⟩
 
+@[simp] lemma coe_one [has_one α] : ((1 : α) : with_bot α) = 1 := rfl
+
 end with_bot
 
 section canonically_ordered_monoid

algebra/ordered_ring.lean

@@ -397,8 +397,8 @@ begin
 end
 
 private lemma one_mul' : ∀a : with_top α, 1 * a = a
-| none     := show ((1:α) : with_top α) * ⊤ = ⊤, by simp
-| (some a) := show ((1:α) : with_top α) * a = a, by simp [coe_mul.symm]
+| none     := show ((1:α) : with_top α) * ⊤ = ⊤, by simp [-with_bot.coe_one]
+| (some a) := show ((1:α) : with_top α) * a = a, by simp [coe_mul.symm, -with_bot.coe_one]
 
 instance [canonically_ordered_comm_semiring α] [decidable_eq α] :
   canonically_ordered_comm_semiring (with_top α) :=

data/nat/basic.lean

@@ -39,6 +39,11 @@ theorem pos_iff_ne_zero : n > 0 ↔ n ≠ 0 :=
 
 theorem pos_iff_ne_zero' : 0 < n ↔ n ≠ 0 := pos_iff_ne_zero
 
+lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
+| 0     := dec_trivial
+| 1     := dec_trivial
+| (n+2) := dec_trivial
+
 theorem eq_of_lt_succ_of_not_lt {a b : ℕ} (h1 : a < b + 1) (h2 : ¬ a < b) : a = b :=
 have h3 : a ≤ b, from le_of_lt_succ h1,
 or.elim (eq_or_lt_of_not_lt h2) (λ h, h) (λ h, absurd h (not_lt_of_ge h3))
@@ -835,5 +840,23 @@ lemma exists_eq_add_of_lt : ∀ {m n : ℕ}, m < n → ∃ k : ℕ, n = m + k +
 | 0 (n+1) h := ⟨n, by simp⟩
 | (m+1) (n+1) h := let ⟨k, hk⟩ := exists_eq_add_of_le (nat.le_of_succ_le_succ h) in ⟨k, by simp [hk]⟩
 
+lemma with_bot.add_eq_zero_iff : ∀ {n m : with_bot ℕ}, n + m = 0 ↔ n = 0 ∧ m = 0
+| none     m        := iff_of_false dec_trivial (λ h, absurd h.1 dec_trivial)
+| n        none     := iff_of_false (by cases n; exact dec_trivial)
+  (λ h, absurd h.2 dec_trivial)
+| (some n) (some m) := show (n + m : with_bot ℕ) = (0 : ℕ) ↔ (n : with_bot ℕ) = (0 : ℕ) ∧
+    (m : with_bot ℕ) = (0 : ℕ),
+  by rw [← with_bot.coe_add, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
+    with_bot.coe_eq_coe, add_eq_zero_iff' (nat.zero_le _) (nat.zero_le _)]
+
+lemma with_bot.add_eq_one_iff : ∀ {n m : with_bot ℕ}, n + m = 1 ↔ (n = 0 ∧ m = 1) ∨ (n = 1 ∧ m = 0)
+| none     none     := dec_trivial
+| none     (some m) := dec_trivial
+| (some n) none     := iff_of_false dec_trivial (λ h, h.elim (λ h, absurd h.2 dec_trivial)
+  (λ h, absurd h.2 dec_trivial))
+| (some n) (some 0) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
+    with_bot.coe_eq_coe]; simp
+| (some n) (some (m + 1)) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
+    with_bot.coe_eq_coe, with_bot.coe_eq_coe]; simp [nat.add_succ, nat.succ_inj', nat.succ_ne_zero]
 
 end nat

data/nat/prime.lean

@@ -19,6 +19,9 @@ theorem prime.ge_two {p : ℕ} : prime p → p ≥ 2 := and.left
 
 theorem prime.gt_one {p : ℕ} : prime p → p > 1 := prime.ge_two
 
+lemma prime.ne_one {p : ℕ} (hp : p.prime) : p ≠ 1 :=
+ne.symm $ (ne_of_lt hp.gt_one)
+
 theorem prime_def_lt {p : ℕ} : prime p ↔ p ≥ 2 ∧ ∀ m < p, m ∣ p → m = 1 :=
 and_congr_right $ λ p2, forall_congr $ λ m,
 ⟨λ h l d, (h d).resolve_right (ne_of_lt l),

data/polynomial.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Jens Wagemaker
 
 Theory of univariate polynomials, represented as `ℕ →₀ α`, where α is a commutative semiring.
 -/
-import data.finsupp algebra.euclidean_domain tactic.ring
+import data.finsupp algebra.euclidean_domain tactic.ring ring_theory.associated
 
 /-- `polynomial α` is the type of univariate polynomials over `α`.
 
@@ -81,6 +81,7 @@ lemma single_eq_C_mul_X : ∀{n}, single n a = C a * X^n
 lemma sum_C_mul_X_eq (p : polynomial α) : p.sum (λn a, C a * X^n) = p :=
 eq.trans (sum_congr rfl $ assume n hn, single_eq_C_mul_X.symm) (finsupp.sum_single _)
 
+
 @[elab_as_eliminator] protected lemma induction_on {M : polynomial α → Prop} (p : polynomial α)
   (h_C : ∀a, M (C a))
   (h_add : ∀p q, M p → M q → M (p + q))
@@ -131,6 +132,8 @@ by simp [coeff, eq_comm, C, single]; congr
 
 @[simp] lemma coeff_X_one : coeff (X : polynomial α) 1 = 1 := rfl
 
+@[simp] lemma coeff_X_zero : coeff (X : polynomial α) 0 = 0 := rfl
+
 @[simp] lemma coeff_C_mul_X (x : α) (k n : ℕ) :
   coeff (C x * X^k : polynomial α) n = if n = k then x else 0 :=
 by rw [← single_eq_C_mul_X]; simp [single, eq_comm, coeff]; congr
@@ -312,6 +315,12 @@ lemma root_mul_right_of_is_root {p : polynomial α} (q : polynomial α) :
   is_root p a → is_root (p * q) a :=
 λ H, by rw [is_root, eval_mul, is_root.def.1 H, zero_mul]
 
+lemma coeff_zero_eq_eval_zero (p : polynomial α) :
+  coeff p 0 = p.eval 0 :=
+calc coeff p 0 = coeff p 0 * 0 ^ 0 : by simp
+... = p.eval 0 : eq.symm $
+  finset.sum_eq_single _ (λ b _ hb, by simp [zero_pow (nat.pos_of_ne_zero hb)]) (by simp)
+
 end eval
 
 section comp
@@ -424,6 +433,12 @@ let ⟨n, hn⟩ :=
 have hn : degree p = some n := not_not.1 hn,
 by rw [nat_degree, hn]; refl
 
+lemma nat_degree_eq_of_degree_eq_some {p : polynomial α} {n : ℕ}
+  (h : degree p = n) : nat_degree p = n :=
+have hp0 : p ≠ 0, from λ hp0, by rw hp0 at h; exact option.no_confusion h,
+option.some_inj.1 $ show (nat_degree p : with_bot ℕ) = n,
+  by rwa [← degree_eq_nat_degree hp0]
+
 @[simp] lemma degree_le_nat_degree : degree p ≤ nat_degree p :=
 begin
   by_cases hp : p = 0, { rw hp, exact bot_le },
@@ -579,6 +594,8 @@ leading_coeff_monomial a 0
 suffices leading_coeff (C (1:α) * X^1) = 1, by rwa [C_1, pow_one, one_mul] at this,
 leading_coeff_monomial 1 1
 
+@[simp] lemma monic_X : monic (X : polynomial α) := leading_coeff_X
+
 @[simp] lemma leading_coeff_one : leading_coeff (1 : polynomial α) = 1 :=
 suffices leading_coeff (C (1:α) * X^0) = 1, by rwa [C_1, pow_zero, mul_one] at this,
 leading_coeff_monomial 1 0
@@ -710,6 +727,13 @@ else with_bot.coe_le_coe.1 $
         (le_nat_degree_of_ne_zero (finsupp.mem_support_iff.1 hn))
         (nat.zero_le _))
 
+lemma zero_le_degree_iff {p : polynomial α} : 0 ≤ degree p ↔ p ≠ 0 :=
+by rw [ne.def, ← degree_eq_bot];
+  cases degree p; exact dec_trivial
+
+@[simp] lemma coeff_mul_X_zero (p : polynomial α) : coeff (p * X) 0 = 0 :=
+by rw [coeff_mul_left, sum_range_succ]; simp
+
 end comm_semiring
 
 section comm_ring
@@ -992,6 +1016,12 @@ lemma dvd_iff_mod_by_monic_eq_zero (hq : monic q) : p %ₘ q = 0 ↔ q ∣ p :=
       degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this;
     exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this))⟩
 
+@[simp] lemma mod_by_monic_one (p : polynomial α) : p %ₘ 1 = 0 :=
+(dvd_iff_mod_by_monic_eq_zero monic_one).2 (one_dvd _)
+
+@[simp] lemma div_by_monic_one (p : polynomial α) : p /ₘ 1 = p :=
+by conv_rhs { rw [← mod_by_monic_add_div p monic_one] }; simp
+
 lemma degree_pos_of_root (hp : p ≠ 0) (h : is_root p a) : 0 < degree p :=
 lt_of_not_ge $ λ hlt, begin
   have := eq_C_of_degree_le_zero hlt,
@@ -1024,6 +1054,9 @@ begin
   refl
 end
 
+lemma X_ne_zero : (X : polynomial α) ≠ 0 :=
+mt (congr_arg (λ p, coeff p 1)) (by simp)
+
 @[simp] lemma degree_X_sub_C (a : α) : degree (X - C a) = 1 :=
 begin
   rw [sub_eq_add_neg, add_comm, ← @degree_X α],
@@ -1099,6 +1132,9 @@ lemma dvd_iff_is_root : (X - C a) ∣ p ↔ is_root p a :=
     mod_by_monic_X_sub_C_eq_C_eval, ← C_0, C_inj] at h,
   λ h, ⟨(p /ₘ (X - C a)), by rw mul_div_by_monic_eq_iff_is_root.2 h⟩⟩
 
+lemma mod_by_monic_X (p : polynomial α) : p %ₘ X = C (p.eval 0) :=
+by rw [← mod_by_monic_X_sub_C_eq_C_eval, C_0, sub_zero]
+
 end nonzero_comm_ring
 
 section integral_domain
@@ -1140,6 +1176,12 @@ instance : integral_domain (polynomial α) :=
   end,
   ..polynomial.nonzero_comm_ring }
 
+lemma nat_degree_mul_eq (hp : p ≠ 0) (hq : q ≠ 0) : nat_degree (p * q) =
+  nat_degree p + nat_degree q :=
+by rw [← with_bot.coe_eq_coe, ← degree_eq_nat_degree (mul_ne_zero hp hq),
+    with_bot.coe_add, ← degree_eq_nat_degree hp,
+    ← degree_eq_nat_degree hq, degree_mul_eq]
+
 @[simp] lemma nat_degree_pow_eq (p : polynomial α) (n : ℕ) :
   nat_degree (p ^ n) = n * nat_degree p :=
 if hp0 : p = 0
@@ -1285,13 +1327,53 @@ lemma leading_coeff_comp (hq : nat_degree q ≠ 0): leading_coeff (p.comp q) =
   leading_coeff p * leading_coeff q ^ nat_degree p :=
 by rw [← coeff_comp_degree_mul_degree hq, ← nat_degree_comp]; refl
 
+lemma degree_eq_zero_of_is_unit (h : is_unit p) : degree p = 0 :=
+let ⟨q, hq⟩ := is_unit_iff_dvd_one.1 h in
+have hp0 : p ≠ 0, from λ hp0, by simpa [hp0] using hq,
+have hq0 : q ≠ 0, from λ hp0, by simpa [hp0] using hq,
+have nat_degree (1 : polynomial α) = nat_degree (p * q),
+  from congr_arg _ hq,
+by rw [nat_degree_one, nat_degree_mul_eq hp0 hq0, eq_comm,
+    add_eq_zero_iff, ← with_bot.coe_eq_coe,
+    ← degree_eq_nat_degree hp0] at this;
+  exact this.1
+
 end integral_domain
 
 section field
 variables [discrete_field α] {p q : polynomial α}
 instance : vector_space α (polynomial α) :=
 { ..finsupp.to_module ℕ α }
 
+lemma is_unit_iff_degree_eq_zero : is_unit p ↔ degree p = 0 :=
+⟨degree_eq_zero_of_is_unit,
+  λ h, have degree p ≤ 0, by simp [*, le_refl],
+    have hc : coeff p 0 ≠ 0, from λ hc,
+        by rw [eq_C_of_degree_le_zero this, hc] at h;
+        simpa using h,
+    is_unit_iff_dvd_one.2 ⟨C (coeff p 0)⁻¹, begin
+      conv in p { rw eq_C_of_degree_le_zero this },
+      rw [← C_mul, _root_.mul_inv_cancel hc, C_1]
+    end⟩⟩
+
+lemma degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬is_unit p) :
+  0 < degree p :=
+lt_of_not_ge (λ h, by rw [eq_C_of_degree_le_zero h] at hp0 hp;
+  exact hp ⟨units.map C (units.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))), rfl⟩)
+
+lemma irreducible_of_degree_eq_one (hp1 : degree p = 1) : irreducible p :=
+⟨mt is_unit_iff_dvd_one.1 (λ ⟨q, hq⟩,
+  absurd (congr_arg degree hq) (λ h,
+    have degree q = 0, by rw [degree_one, degree_mul_eq, hp1, eq_comm,
+      nat.with_bot.add_eq_zero_iff] at h; exact h.2,
+    by simp [degree_mul_eq, this, degree_one, hp1] at h;
+      exact absurd h dec_trivial)),
+λ q r hpqr, begin
+  have := congr_arg degree hpqr,
+  rw [hp1, degree_mul_eq, eq_comm, nat.with_bot.add_eq_one_iff] at this,
+  rw [is_unit_iff_degree_eq_zero, is_unit_iff_degree_eq_zero]; tautology
+end⟩
+
 lemma monic_mul_leading_coeff_inv (h : p ≠ 0) :
   monic (p * C (leading_coeff p)⁻¹) :=
 by rw [monic, leading_coeff_mul, leading_coeff_C,

data/zmod/quadratic_reciprocity.lean

@@ -9,12 +9,12 @@ open function finset nat finite_field zmodp
 
 namespace zmodp
 
-variables {p q : ℕ} (hp : prime p) (hq : prime q)
+variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
 
 @[simp] lemma card_units_zmodp : fintype.card (units (zmodp p hp)) = p - 1 :=
 by rw [card_units, card_zmodp]
 
-theorem fermat_little {p : ℕ} (hp : prime p) {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p - 1) = 1 :=
+theorem fermat_little {p : ℕ} (hp : nat.prime p) {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p - 1) = 1 :=
 by rw [← units.mk0_val ha, ← @units.coe_one (zmodp p hp), ← units.coe_pow, ← units.ext_iff,
     ← card_units_zmodp hp, pow_card_eq_one]
 
@@ -47,7 +47,7 @@ hp.eq_two_or_odd.elim
   (λ hp1, by rw [← mul_self_eq_one_iff, ← _root_.pow_add, ← two_mul, two_mul_odd_div_two hp1];
     exact fermat_little hp ha)
 
-@[simp] lemma wilsons_lemma {p : ℕ} (hp : prime p) : (fact (p - 1) : zmodp p hp) = -1 :=
+@[simp] lemma wilsons_lemma {p : ℕ} (hp : nat.prime p) : (fact (p - 1) : zmodp p hp) = -1 :=
 begin
   rw [← finset.prod_range_id_eq_fact, ← @units.coe_one (zmodp p hp), ← units.coe_neg,
     ← @prod_univ_units_id_eq_neg_one (zmodp p hp),
@@ -66,7 +66,7 @@ begin
       by simp [val_cast_of_lt hp this.2]⟩))
 end
 
-@[simp] lemma prod_range_prime_erase_zero {p : ℕ} (hp : prime p) :
+@[simp] lemma prod_range_prime_erase_zero {p : ℕ} (hp : nat.prime p) :
   ((range p).erase 0).prod (λ x, (x : zmodp p hp)) = -1 :=
 by conv in (range p) { rw [← succ_sub_one p, succ_sub hp.pos] };
   rw [prod_hom (coe : ℕ → zmodp p hp) nat.cast_one nat.cast_mul,
@@ -76,7 +76,7 @@ end zmodp
 
 namespace quadratic_reciprocity_aux
 
-variables {p q : ℕ} (hp : prime p) (hq : prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1)
+variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1)
   (hpq : p ≠ q)
 
 include hp hq hp1 hq1 hpq
@@ -115,7 +115,7 @@ finset.ext.2 $ λ x,
             ← nat.sub_add_comm (mul_pos hp.pos hq.pos), add_succ, succ_eq_add_one, nat.add_sub_cancel];
           exact le_trans (nat.sub_le_self _ _) (nat.le_add_right _ _),
     end,
-  by rw [prime.coprime_iff_not_dvd hp, ← hk₂, ← nat.dvd_add_iff_left (dvd_mul_right _ _),
+  by rw [nat.prime.coprime_iff_not_dvd hp, ← hk₂, ← nat.dvd_add_iff_left (dvd_mul_right _ _),
        dvd_iff_mod_eq_zero, mod_eq_of_lt]; clear _let_match _let_match; simp at hk₁; tauto⟩)
   (λ h, let ⟨m, hm₁, hm₂⟩ := mem_image.1 h in ⟨mem_range.2 $ hm₂ ▸ begin
     refine (mul_lt_mul_left (show 0 < 2, from  dec_trivial)).1 _,
@@ -219,7 +219,7 @@ begin
         by rw nat.div_mul_cancel hb'.2⟩))
 end
 
-lemma prod_range_p_mul_q_filter_coprime_mod_p (hq : prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
+lemma prod_range_p_mul_q_filter_coprime_mod_p (hq : nat.prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
   ((((range ((p * q) / 2).succ).filter (coprime (p * q))).prod (λ x, x) : ℕ) : zmodp p hp) =
   (-1) ^ (q / 2) * q ^ (p / 2) :=
 have hq0 : (q : zmodp p hp) ≠ 0, by rwa [← nat.cast_zero, ne.def, zmodp.eq_iff_modeq_nat, nat.modeq.modeq_zero_iff,
@@ -294,7 +294,7 @@ have hinj : ∀ a₁ a₂ : ℕ,
       by simpa [lt_succ_iff, coprime_mul_iff_left] using hb,
     have hbpq' : b < ((⟨p * q, mul_pos hp.pos hq.pos⟩ : ℕ+) : ℕ) :=
       lt_of_le_of_lt hb'.1 (div_lt_self (mul_pos hp.pos hq.pos) dec_trivial),
-    have val_inj : ∀ {p : ℕ} (hp : prime p) (x y : zmodp p hp), x.val = y.val ↔ x = y,
+    have val_inj : ∀ {p : ℕ} (hp : nat.prime p) (x y : zmodp p hp), x.val = y.val ↔ x = y,
       from λ _ _ _ _, ⟨fin.eq_of_veq, fin.veq_of_eq⟩,
     have hbpq0 : (b : zmod (⟨p * q, mul_pos hp.pos hq.pos⟩)) ≠ 0,
       by rw [ne.def, zmod.eq_zero_iff_dvd_nat];
@@ -322,9 +322,9 @@ have hmem : ∀ a : ℕ,
     (if (a : zmodp q hq).1 ≤ q / 2 then ((a : zmodp p hp).1, (a : zmodp q hq).1)
       else ((-a : zmodp p hp).1, (-a : zmodp q hq).1)) ∈
       ((range p).erase 0).product ((range (succ (q / 2))).erase 0),
-  from λ x, have hxp : ∀ {p : ℕ} (hp : prime p), (x : zmodp p hp).val = 0 ↔ p ∣ x,
+  from λ x, have hxp : ∀ {p : ℕ} (hp : nat.prime p), (x : zmodp p hp).val = 0 ↔ p ∣ x,
     from λ p hp, by rw [zmodp.val_cast_nat, nat.dvd_iff_mod_eq_zero],
-  have hxpneg : ∀ {p : ℕ} (hp : prime p), (-x : zmodp p hp).val = 0 ↔ p ∣ x,
+  have hxpneg : ∀ {p : ℕ} (hp : nat.prime p), (-x : zmodp p hp).val = 0 ↔ p ∣ x,
     from λ p hp, by rw [← int.cast_coe_nat x, ← int.cast_neg, ← int.coe_nat_inj',
       zmodp.coe_val_cast_int, int.coe_nat_zero, ← int.dvd_iff_mod_eq_zero, dvd_neg, int.coe_nat_dvd],
   have hxplt : (x : zmodp p hp).val < p := (x : zmodp p hp).2,
@@ -451,32 +451,32 @@ end quadratic_reciprocity_aux
 
 open quadratic_reciprocity_aux
 
-variables {p q : ℕ} (hp : prime p) (hq : prime q)
+variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
 
 namespace zmodp
 
-def legendre_sym (a p : ℕ) (hp : prime p) : ℤ :=
+def legendre_sym (a p : ℕ) (hp : nat.prime p) : ℤ :=
 if (a : zmodp p hp) = 0 then 0 else if ∃ b : zmodp p hp, b ^ 2 = a then 1 else -1
 
-lemma legendre_sym_eq_pow (a p : ℕ) (hp : prime p) : (legendre_sym a p hp : zmodp p hp) = (a ^ (p / 2)) :=
+lemma legendre_sym_eq_pow (a p : ℕ) (hp : nat.prime p) : (legendre_sym a p hp : zmodp p hp) = (a ^ (p / 2)) :=
 if ha : (a : zmodp p hp) = 0 then by simp [*, legendre_sym, _root_.zero_pow (nat.div_pos hp.ge_two (succ_pos 1))]
 else
-(prime.eq_two_or_odd hp).elim
+(nat.prime.eq_two_or_odd hp).elim
   (λ hp2, begin subst hp2,
-    suffices : ∀ a : zmodp 2 prime_two,
-      (((ite (a = 0) 0 (ite (∃ (b : zmodp 2 hp), b ^ 2 = a) 1 (-1))) : ℤ) : zmodp 2 prime_two) = a ^ (2 / 2),
+    suffices : ∀ a : zmodp 2 nat.prime_two,
+      (((ite (a = 0) 0 (ite (∃ (b : zmodp 2 hp), b ^ 2 = a) 1 (-1))) : ℤ) : zmodp 2 nat.prime_two) = a ^ (2 / 2),
     { exact this a },
     exact dec_trivial,
    end)
   (λ hp1, have _ := euler_criterion hp ha,
     have (-1 : zmodp p hp) ≠ 1, from (ne_neg_self hp hp1 zero_ne_one.symm).symm,
     by cases zmodp.pow_div_two_eq_neg_one_or_one hp ha; simp [legendre_sym, *] at *)
 
-lemma legendre_sym_eq_one_or_neg_one (a : ℕ) (hp : prime p) (ha : (a : zmodp p hp) ≠ 0) :
+lemma legendre_sym_eq_one_or_neg_one (a : ℕ) (hp : nat.prime p) (ha : (a : zmodp p hp) ≠ 0) :
   legendre_sym a p hp = -1 ∨ legendre_sym a p hp = 1 :=
 by unfold legendre_sym; split_ifs; simp * at *
 
-theorem quadratic_reciprocity (hp : prime p) (hq : prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
+theorem quadratic_reciprocity (hp : nat.prime p) (hq : nat.prime q) (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
   legendre_sym p q hq * legendre_sym q p hp = (-1) ^ ((p / 2) * (q / 2)) :=
 have hneg_one_or_one : ((range (p * q / 2).succ).filter (coprime (p * q))).prod
     (λ (x : ℕ), if (x : zmodp q hq).val ≤ q / 2 then (1 : zmodp p hp × zmodp q hq) else -1) = 1 ∨