feat(number_theory/divisors): add nat.cons_self_proper_divisors (#1…

…8176)

* Rename `nat.divisors_eq_proper_divisors_insert_self_of_pos` to `nat.insert_self_proper_divisors`, assume `n ≠ 0` instead of `0 < n` and swap LHS with RHS.
* Add `nat.cons_self_proper_divisors`. This is easier to use with `finset.prod_cons`/`finset.sum_cons`.

src/data/finset/basic.lean

@@ -1251,6 +1251,10 @@ theorem erase_insert_of_ne {a b : α} {s : finset α} (h : a ≠ b) :
 ext $ λ x, have x ≠ b ∧ x = a ↔ x = a, from and_iff_right_of_imp (λ hx, hx.symm ▸ h),
 by simp only [mem_erase, mem_insert, and_or_distrib_left, this]
 
+theorem erase_cons_of_ne {a b : α} {s : finset α} (ha : a ∉ s) (hb : a ≠ b) :
+  erase (cons a s ha) b = cons a (erase s b) (λ h, ha $ erase_subset _ _ h) :=
+by simp only [cons_eq_insert, erase_insert_of_ne hb]
+
 theorem insert_erase {a : α} {s : finset α} (h : a ∈ s) : insert a (erase s a) = s :=
 ext $ assume x, by simp only [mem_insert, mem_erase, or_and_distrib_left, dec_em, true_and];
 apply or_iff_right_of_imp; rintro rfl; exact h

src/group_theory/order_of_element.lean

@@ -571,7 +571,7 @@ variables [monoid G]
 open_locale big_operators
 
 @[to_additive sum_card_add_order_of_eq_card_nsmul_eq_zero]
-lemma sum_card_order_of_eq_card_pow_eq_one [fintype G] [decidable_eq G] (hn : 0 < n) :
+lemma sum_card_order_of_eq_card_pow_eq_one [fintype G] [decidable_eq G] (hn : n ≠ 0) :
   ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ x : G, order_of x = m)).card
   = (finset.univ.filter (λ x : G, x ^ n = 1)).card :=
 calc ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ x : G, order_of x = m)).card
@@ -581,7 +581,7 @@ calc ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ x :
   suffices : order_of x ≤ n ∧ order_of x ∣ n ↔ x ^ n = 1,
   { simpa [nat.lt_succ_iff], },
   exact ⟨λ h, let ⟨m, hm⟩ := h.2 in by rw [hm, pow_mul, pow_order_of_eq_one, one_pow],
-    λ h, ⟨order_of_le_of_pow_eq_one hn h, order_of_dvd_of_pow_eq_one h⟩⟩
+    λ h, ⟨order_of_le_of_pow_eq_one hn.bot_lt h, order_of_dvd_of_pow_eq_one h⟩⟩
 end))
 
 end finite_monoid

src/group_theory/specific_groups/cyclic.lean

@@ -297,24 +297,24 @@ private lemma card_order_of_eq_totient_aux₁ :
   ∀ {d : ℕ}, d ∣ fintype.card α → 0 < (univ.filter (λ a : α, order_of a = d)).card →
   (univ.filter (λ a : α, order_of a = d)).card = φ d :=
 begin
-  intros d hd hd0,
+  intros d hd hpos,
   induction d using nat.strong_rec' with d IH,
-  rcases d.eq_zero_or_pos with rfl | hd_pos,
+  rcases decidable.eq_or_ne d 0 with rfl | hd0,
   { cases fintype.card_ne_zero (eq_zero_of_zero_dvd hd) },
-  rcases card_pos.1 hd0 with ⟨a, ha'⟩,
+  rcases card_pos.1 hpos with ⟨a, ha'⟩,
   have ha : order_of a = d := (mem_filter.1 ha').2,
   have h1 : ∑ m in d.proper_divisors, (univ.filter (λ a : α, order_of a = m)).card =
     ∑ m in d.proper_divisors, φ m,
   { refine finset.sum_congr rfl (λ m hm, _),
     simp only [mem_filter, mem_range, mem_proper_divisors] at hm,
     refine IH m hm.2 (hm.1.trans hd) (finset.card_pos.2 ⟨a ^ (d / m), _⟩),
     simp only [mem_filter, mem_univ, order_of_pow a, ha, true_and,
-      nat.gcd_eq_right (div_dvd_of_dvd hm.1), nat.div_div_self hm.1 hd_pos.ne'] },
+      nat.gcd_eq_right (div_dvd_of_dvd hm.1), nat.div_div_self hm.1 hd0] },
   have h2 : ∑ m in d.divisors, (univ.filter (λ a : α, order_of a = m)).card =
     ∑ m in d.divisors, φ m,
-    { rw [←filter_dvd_eq_divisors hd_pos.ne', sum_card_order_of_eq_card_pow_eq_one hd_pos,
-      filter_dvd_eq_divisors hd_pos.ne', sum_totient, ←ha, card_pow_eq_one_eq_order_of_aux hn a] },
-  simpa [divisors_eq_proper_divisors_insert_self_of_pos hd_pos, ←h1] using h2,
+    { rw [←filter_dvd_eq_divisors hd0, sum_card_order_of_eq_card_pow_eq_one hd0,
+      filter_dvd_eq_divisors hd0, sum_totient, ←ha, card_pow_eq_one_eq_order_of_aux hn a] },
+  simpa [← cons_self_proper_divisors hd0, ←h1] using h2,
 end
 
 lemma card_order_of_eq_totient_aux₂ {d : ℕ} (hd : d ∣ fintype.card α) :
@@ -328,7 +328,7 @@ begin
   apply lt_irrefl c,
   calc
     c = ∑ m in c.divisors, (univ.filter (λ a : α, order_of a = m)).card : by
-  { simp only [←filter_dvd_eq_divisors hc0.ne', sum_card_order_of_eq_card_pow_eq_one hc0],
+  { simp only [←filter_dvd_eq_divisors hc0.ne', sum_card_order_of_eq_card_pow_eq_one hc0.ne'],
     apply congr_arg card,
     simp }
   ... = ∑ m in c.divisors.erase d, (univ.filter (λ a : α, order_of a = m)).card : by

src/number_theory/divisors.lean

@@ -77,10 +77,13 @@ begin
   simp only [and_comm, ←filter_dvd_eq_proper_divisors hm, mem_filter, mem_range],
 end
 
-lemma divisors_eq_proper_divisors_insert_self_of_pos (h : 0 < n):
-  divisors n = has_insert.insert n (proper_divisors n) :=
-by rw [divisors, proper_divisors, Ico_succ_right_eq_insert_Ico h, finset.filter_insert,
-  if_pos (dvd_refl n)]
+lemma insert_self_proper_divisors (h : n ≠ 0): insert n (proper_divisors n) = divisors n :=
+by rw [divisors, proper_divisors, Ico_succ_right_eq_insert_Ico (one_le_iff_ne_zero.2 h),
+  finset.filter_insert, if_pos (dvd_refl n)]
+
+lemma cons_self_proper_divisors (h : n ≠ 0) :
+  cons n (proper_divisors n) proper_divisors.not_self_mem = divisors n :=
+by rw [cons_eq_insert, insert_self_proper_divisors h]
 
 @[simp]
 lemma mem_divisors {m : ℕ} : n ∈ divisors m ↔ (n ∣ m ∧ m ≠ 0) :=
@@ -245,10 +248,9 @@ end
 lemma sum_divisors_eq_sum_proper_divisors_add_self :
   ∑ i in divisors n, i = ∑ i in proper_divisors n, i + n :=
 begin
-  cases n,
+  rcases decidable.eq_or_ne n 0 with rfl|hn,
   { simp },
-  { rw [divisors_eq_proper_divisors_insert_self_of_pos (nat.succ_pos _),
-        finset.sum_insert (proper_divisors.not_self_mem), add_comm] }
+  { rw [← cons_self_proper_divisors hn, finset.sum_cons, add_comm] }
 end
 
 /-- `n : ℕ` is perfect if and only the sum of the proper divisors of `n` is `n` and `n`
@@ -280,8 +282,7 @@ end
 
 lemma prime.proper_divisors {p : ℕ} (pp : p.prime) :
   proper_divisors p = {1} :=
-by rw [← erase_insert (proper_divisors.not_self_mem),
-    ← divisors_eq_proper_divisors_insert_self_of_pos pp.pos,
+by rw [← erase_insert proper_divisors.not_self_mem, insert_self_proper_divisors pp.ne_zero,
     pp.divisors, pair_comm, erase_insert (λ con, pp.ne_one (mem_singleton.1 con))]
 
 lemma divisors_prime_pow {p : ℕ} (pp : p.prime) (k : ℕ) :
@@ -335,8 +336,7 @@ by simp [h.proper_divisors]
 @[simp, to_additive]
 lemma prime.prod_divisors {α : Type*} [comm_monoid α] {p : ℕ} {f : ℕ → α} (h : p.prime) :
   ∏ x in p.divisors, f x = f p * f 1 :=
-by rw [divisors_eq_proper_divisors_insert_self_of_pos h.pos,
-       prod_insert proper_divisors.not_self_mem, h.prod_proper_divisors]
+by rw [← cons_self_proper_divisors h.ne_zero, prod_cons, h.prod_proper_divisors]
 
 lemma proper_divisors_eq_singleton_one_iff_prime :
   n.proper_divisors = {1} ↔ n.prime :=

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -180,9 +180,8 @@ lemma cyclotomic'_eq_X_pow_sub_one_div {K : Type*} [comm_ring K] [is_domain K] {
   (hpos : 0 < n) (h : is_primitive_root ζ n) :
   cyclotomic' n K = (X ^ n - 1) /ₘ (∏ i in nat.proper_divisors n, cyclotomic' i K) :=
 begin
-  rw [←prod_cyclotomic'_eq_X_pow_sub_one hpos h,
-  nat.divisors_eq_proper_divisors_insert_self_of_pos hpos,
-  finset.prod_insert nat.proper_divisors.not_self_mem],
+  rw [←prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← nat.cons_self_proper_divisors hpos.ne',
+    finset.prod_cons],
   have prod_monic : (∏ i in nat.proper_divisors n, cyclotomic' i K).monic,
   { apply monic_prod_of_monic,
     intros i hi,
@@ -224,12 +223,9 @@ begin
   let Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁,
   have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree,
   { split,
-    { rw [zero_add, mul_comm, ←(prod_cyclotomic'_eq_X_pow_sub_one hpos h),
-      nat.divisors_eq_proper_divisors_insert_self_of_pos hpos],
-      simp only [true_and, finset.prod_insert, not_lt, nat.mem_proper_divisors, dvd_refl] },
-    rw [degree_zero, bot_lt_iff_ne_bot],
-    intro habs,
-    exact (monic.ne_zero Bmo) (degree_eq_bot.1 habs) },
+    { rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h,
+         ← nat.cons_self_proper_divisors hpos.ne', finset.prod_cons] },
+    { simpa only [degree_zero, bot_lt_iff_ne_bot, ne.def, degree_eq_bot] using Bmo.ne_zero } },
   replace huniq := div_mod_by_monic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq,
   simp only [lifts, ring_hom.mem_srange],
   use Q₁,
@@ -448,8 +444,7 @@ begin
   convert X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h using 1,
   rw mul_assoc,
   congr' 1,
-  rw [nat.divisors_eq_proper_divisors_insert_self_of_pos $ pos_of_gt hdn,
-      finset.insert_sdiff_of_not_mem, finset.prod_insert],
+  rw [← nat.insert_self_proper_divisors hdn.ne_bot, insert_sdiff_of_not_mem, prod_insert],
   { exact finset.not_mem_sdiff_of_not_mem_left nat.proper_divisors.not_self_mem },
   { exact λ hk, hdn.not_le $ nat.divisor_le hk }
 end
@@ -503,9 +498,8 @@ lemma cyclotomic_eq_X_pow_sub_one_div {R : Type*} [comm_ring R] {n : ℕ}
   (hpos: 0 < n) : cyclotomic n R = (X ^ n - 1) /ₘ (∏ i in nat.proper_divisors n, cyclotomic i R) :=
 begin
   nontriviality R,
-  rw [←prod_cyclotomic_eq_X_pow_sub_one hpos,
-  nat.divisors_eq_proper_divisors_insert_self_of_pos hpos,
-  finset.prod_insert nat.proper_divisors.not_self_mem],
+  rw [←prod_cyclotomic_eq_X_pow_sub_one hpos, ← nat.cons_self_proper_divisors hpos.ne',
+    finset.prod_cons],
   have prod_monic : (∏ i in nat.proper_divisors n, cyclotomic i R).monic,
   { apply monic_prod_of_monic,
     intros i hi,
@@ -670,9 +664,8 @@ lemma eq_cyclotomic_iff {R : Type*} [comm_ring R] {n : ℕ} (hpos: 0 < n)
 begin
   nontriviality R,
   refine ⟨λ hcycl, _, λ hP, _⟩,
-  { rw [hcycl, ← finset.prod_insert (@nat.proper_divisors.not_self_mem n),
-      ← nat.divisors_eq_proper_divisors_insert_self_of_pos hpos],
-    exact prod_cyclotomic_eq_X_pow_sub_one hpos R },
+  { rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← nat.cons_self_proper_divisors hpos.ne',
+        finset.prod_cons] },
   { have prod_monic : (∏ i in nat.proper_divisors n, cyclotomic i R).monic,
     { apply monic_prod_of_monic,
       intros i hi,
@@ -711,7 +704,7 @@ lemma cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type*) [comm_ring R] (p k : 
 by rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
 
 /-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`. -/
-lemma cyclotomic_coeff_zero (R : Type*) [comm_ring R] {n : ℕ} (hn : 2 ≤ n) :
+lemma cyclotomic_coeff_zero (R : Type*) [comm_ring R] {n : ℕ} (hn : 1 < n) :
   (cyclotomic n R).coeff 0 = 1 :=
 begin
   induction n using nat.strong_induction_on with n hi,
@@ -732,10 +725,9 @@ begin
       simp only [finset.prod_const_one] },
     simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub] },
   have heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0,
-  { rw [←prod_cyclotomic_eq_X_pow_sub_one (lt_of_lt_of_le zero_lt_two hn),
-        nat.divisors_eq_proper_divisors_insert_self_of_pos (lt_of_lt_of_le zero_lt_two hn),
-        finset.prod_insert nat.proper_divisors.not_self_mem, mul_coeff_zero, coeff_zero_prod, hprod,
-        mul_neg, mul_one] },
+  { rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn),
+        ← nat.cons_self_proper_divisors hn.ne_bot, finset.prod_cons, mul_coeff_zero,
+        coeff_zero_prod, hprod, mul_neg, mul_one] },
   have hzero : (X ^ n - 1).coeff 0 = (-1 : R),
   { rw coeff_zero_eq_eval_zero _,
     simp only [zero_pow (lt_of_lt_of_le zero_lt_two hn), eval_X, eval_one, zero_sub, eval_pow,
@@ -780,9 +772,8 @@ begin
     apply units.coe_eq_one.1,
     simp only [sub_eq_zero.mp hpow, zmod.coe_unit_of_coprime, units.coe_pow] },
   rw [is_root.def] at hroot,
-  rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (zmod p),
-    nat.divisors_eq_proper_divisors_insert_self_of_pos hpos,
-    finset.prod_insert nat.proper_divisors.not_self_mem, eval_mul, hroot, zero_mul]
+  rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (zmod p), ← nat.cons_self_proper_divisors hpos.ne',
+    finset.prod_cons, eval_mul, hroot, zero_mul]
 end
 
 end order

src/ring_theory/polynomial/cyclotomic/eval.lean

@@ -71,10 +71,8 @@ begin
   dsimp at ih,
   have := prod_cyclotomic_eq_geom_sum hn' R,
   apply_fun eval x at this,
-  rw [divisors_eq_proper_divisors_insert_self_of_pos hn', finset.erase_insert_of_ne hn''.ne',
-      finset.prod_insert, eval_mul, eval_geom_sum] at this,
-  swap,
-  { simp only [proper_divisors.not_self_mem, mem_erase, and_false, not_false_iff] },
+  rw [← cons_self_proper_divisors hn'.ne', finset.erase_cons_of_ne _ hn''.ne',
+      finset.prod_cons, eval_mul, eval_geom_sum] at this,
   rcases lt_trichotomy 0 (∑ i in finset.range n, x ^ i) with h | h | h,
   { apply pos_of_mul_pos_left,
     { rwa this },