zmod.lean

import data.zmod.basic
import data.fintype.basic
import field_theory.finite.basic
import group_theory.order_of_element

noncomputable instance units_zmod.fintype : Π n, fintype (units (zmod n))
| 0     := units_int.fintype
| (n+1) := units.fintype

lemma finset.not_subset (α : Type*) (s t : finset α) : ¬(s ⊆ t) ↔ ∃ x ∈ s, ¬(x ∈ t) :=
begin
  rw [←finset.coe_subset, set.not_subset],
  simp,
end

lemma finset.eq_of_subset_of_card (α : Type*) (s t : finset α) (h1 : s ⊆ t)  (h2 : s.card = t.card) :
  s = t :=
begin
  classical,
  apply finset.subset.antisymm h1,
  contrapose! h2,
  refine (finset.card_lt_card _).ne,
  rwa [finset.ssubset_iff_of_subset h1, ←finset.not_subset],
end

lemma finset.filter_card_eq (α : Type*) (s : finset α) (p : α → Prop)
  [decidable_pred p]
  (h : (s.filter p).card = s.card) :
  ∀ x ∈ s, p x :=
begin
  have h0 : (finset.filter p s) ⊆ s := finset.filter_subset p s,
  have h1 : finset.filter p s = s := finset.eq_of_subset_of_card _ _ _ h0 h,
  intros x hx,
  rw [←h1, finset.mem_filter] at hx,
  exact hx.2,
end

lemma nat.prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.coprime m) : nat.prime n :=
begin
  refine nat.prime_def_lt.mpr _,
  refine ⟨h1, λ m mlt mdvd, _⟩,
  have h3 : m ≠ 0,
  { rintro rfl,
    rw zero_dvd_iff at mdvd,
    exact mlt.ne' mdvd },
  have h2 := h m mlt h3,
  exact nat.coprime.eq_one_of_dvd h2.symm mdvd,
end

lemma tot (p : ℕ) (h0 : p.totient = p - 1) (h1 : 0 < p) : nat.prime p :=
begin
  have h9 : p ≠ 1,
  { rintro rfl,
    rw [nat.totient_one, nat.sub_self] at h0,
    exact one_ne_zero h0 },
  have h10 : 1 < p,
  { apply lt_of_le_of_ne _ h9.symm,
    rwa nat.succ_le_iff },
  rw nat.totient_eq_card_coprime at h0,
  have := nat.totient_one,
  have h2 : ¬ p.coprime 0,
  { rw nat.coprime_zero_right, exact h10.ne' },
  have h8 : {0} ⊆ finset.range p,
  { rwa [finset.singleton_subset_iff, finset.mem_range] },
  have h5 : finset.range p = {0} ∪ (finset.range p \ {0}) := (finset.union_sdiff_of_subset h8).symm,
  have h6 : finset.filter p.coprime {0} = ∅,
  { ext a,
    simp only [finset.not_mem_empty, not_and, finset.mem_filter, finset.mem_singleton, iff_false],
    rintro rfl,
    exact h2 },
  have h7 : (finset.range p \ {0}).card = p - 1,
  { rw [finset.card_sdiff h8, finset.card_singleton, finset.card_range] },
  rw [h5, finset.filter_union, h6, finset.empty_union, ←h7] at h0,
  refine p.prime_of_coprime h10 (λ n hn hnz, _),
  apply finset.filter_card_eq _ _ _ h0 n,
  rw [finset.mem_sdiff, finset.mem_singleton, finset.mem_range],
  exact ⟨hn, hnz⟩,
end

lemma prime_iff_card_units (p : ℕ) :
  p.prime ↔ fintype.card (units (zmod p)) = p - 1
:=
begin
  split,
    { intro p_prime,
      haveI := fact.mk p_prime,
      convert zmod.card_units p },
    { intro h,
      cases nat.eq_zero_or_pos p with hp hp,
      { exfalso, subst p,
        have h0 : (finset.univ : finset (units (ℤ))) = {1, -1},
        { ext,
          simp [int.units_eq_one_or] },
        have h1 : (finset.univ : finset (units (zmod 0))) = {1, -1} := h0,
        rw [←finset.card_univ, h1] at h,
        simpa using h },
      { haveI := fact.mk hp,
        have : p.totient = p - 1,
        { rw ←h, convert (zmod.card_units_eq_totient p).symm },
        apply tot _ this hp } }
end

Ruben, you can do the last lemma like this:

    { intro h,
      obtain rfl | hp := nat.eq_zero_or_pos p,
      { exfalso,
        have : fintype.card (units (zmod 0)) = 2, from dec_trivial,
        contradiction },
      { haveI := fact.mk hp,
        have : p.totient = p - 1,
        { rw ←h, convert (zmod.card_units_eq_totient p).symm },
        apply tot _ this hp } }

That dec_trivial can even be rfl, but I feel like people would shout about breaking the API