feat(data/zmod): lemmas about totient and zmod (#2158)

* feat(data/zmod): lemmas about totient and zmod

* docstring

* Changes based on Johan's comments

* fix build

* subsingleton (units(zmod 2))

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/fintype.lean

@@ -306,6 +306,9 @@ instance multiplicative.fintype : Π [fintype α], fintype (multiplicative α) :
 
 @[simp] theorem fintype.card_units_int : fintype.card (units ℤ) = 2 := rfl
 
+noncomputable instance [monoid α] [fintype α] : fintype (units α) :=
+by classical; exact fintype.of_injective units.val units.ext
+
 @[simp] theorem fintype.card_bool : fintype.card bool = 2 := rfl
 
 def finset.insert_none (s : finset α) : finset (option α) :=

src/data/nat/totient.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import algebra.big_operators data.nat.gcd
+import algebra.big_operators data.zmod.basic
 
 open finset
 
@@ -13,6 +13,8 @@ def totient (n : ℕ) : ℕ := ((range n).filter (nat.coprime n)).card
 
 localized "notation `φ` := nat.totient" in nat
 
+@[simp] theorem totient_zero : φ 0 = 0 := rfl
+
 lemma totient_le (n : ℕ) : φ n ≤ n :=
 calc totient n ≤ (range n).card : card_le_of_subset (filter_subset _)
            ... = n              : card_range _
@@ -68,3 +70,20 @@ calc ((range n.succ).filter (∣ n)).sum φ
 ... = n : card_range _
 
 end nat
+
+namespace zmod
+
+open fintype
+open_locale nat
+
+@[simp] lemma card_units_eq_totient (n : ℕ+) :
+  card (units (zmod n)) = φ n :=
+calc card (units (zmod n)) = card {x : zmod n // x.1.coprime n} :
+  fintype.card_congr zmod.units_equiv_coprime
+... = φ n : finset.card_congr
+  (λ a _, a.1.1)
+  (λ a, by simp [a.1.2, a.2.symm] {contextual := tt})
+  (λ _ _ h, by simp [subtype.val_injective.eq_iff, (fin.eq_iff_veq _ _).symm])
+  (λ b hb, ⟨⟨⟨b, by finish⟩, nat.coprime.symm (by simp at hb; tauto)⟩, mem_univ _, rfl⟩)
+
+end zmod

src/data/zmod/basic.lean

@@ -217,6 +217,14 @@ instance (n : ℕ+) : has_repr (zmod n) := fin.has_repr _
 
 lemma card_zmod (n : ℕ+) : fintype.card (zmod n) = n := fintype.card_fin n
 
+instance : subsingleton (units (zmod 2)) :=
+⟨λ x y, begin
+  cases x with x xi,
+  cases y with y yi,
+  revert x y xi yi,
+  exact dec_trivial
+end⟩
+
 lemma le_div_two_iff_lt_neg {n : ℕ+} (hn : (n : ℕ) % 2 = 1)
   {x : zmod n} (hx0 : x ≠ 0) : x.1 ≤ (n / 2 : ℕ) ↔ (n / 2 : ℕ) < (-x).1 :=
 have hn2 : (n : ℕ) / 2 < n := nat.div_lt_of_lt_mul ((lt_mul_iff_one_lt_left n.pos).2 dec_trivial),
@@ -253,6 +261,18 @@ let ⟨k , hk⟩ := h in
 zmod.eq_iff_modeq_nat.2 (nat.modeq.modeq_of_modeq_mul_right k
     (by rw [← hk, zmod.val_cast_nat]; exact nat.mod_mod _ _))
 
+/-- `unit_of_coprime` makes an element of `units (zmod n)` given
+  a natural number `x` and a proof that `x` is coprime to `n`  -/
+def unit_of_coprime {n : ℕ+} (x : ℕ) (h : nat.coprime x n) : units (zmod n) :=
+have (x * gcd_a x ↑n : zmod n) = 1,
+  by rw [← int.cast_coe_nat, ← int.cast_one, ← int.cast_mul,
+      zmod.eq_iff_modeq_int, ← int.coe_nat_one, ← (show nat.gcd _ _ = _, from h)];
+    simpa using int.modeq.gcd_a_modeq x n,
+⟨x, gcd_a x n, this, by simpa [mul_comm] using this⟩
+
+@[simp] lemma cast_unit_of_coprime {n : ℕ+} (x : ℕ) (h : nat.coprime x n) :
+  (unit_of_coprime x h : zmod n) = x := rfl
+
 def units_equiv_coprime {n : ℕ+} : units (zmod n) ≃ {x : zmod n // nat.coprime x.1 n} :=
 { to_fun := λ x, ⟨x, nat.modeq.coprime_of_mul_modeq_one (x⁻¹).1.1 begin
     have := units.ext_iff.1 (mul_right_inv x),
@@ -261,14 +281,9 @@ def units_equiv_coprime {n : ℕ+} : units (zmod n) ≃ {x : zmod n // nat.copri
       units.coe_mul, zmod.mul_val, zmod.cast_mod_nat, zmod.cast_mod_nat,
       zmod.eq_iff_modeq_nat] at this
     end⟩,
-  inv_fun := λ x,
-    have x.val * ↑(gcd_a ((x.val).val) ↑n) = 1,
-      by rw [← zmod.cast_val x.1, ← int.cast_coe_nat, ← int.cast_one, ← int.cast_mul,
-          zmod.eq_iff_modeq_int, ← int.coe_nat_one, ← (show nat.gcd _ _ = _, from x.2)];
-        simpa using int.modeq.gcd_a_modeq x.1.1 n,
-    ⟨x.1, gcd_a x.1.1 n, this, by simpa [mul_comm] using this⟩,
-  left_inv := λ ⟨_, _, _, _⟩, units.ext rfl,
-  right_inv := λ ⟨_, _⟩, rfl }
+  inv_fun := λ x, unit_of_coprime x.1.1 x.2,
+  left_inv := λ ⟨_, _, _, _⟩, units.ext (by simp),
+  right_inv := λ ⟨_, _⟩, by simp }
 
 /-- `val_min_abs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
   The result will be in the interval `(-n/2, n/2]` -/
@@ -437,6 +452,9 @@ instance : fintype (zmodp p hp) := @zmod.fintype ⟨p, hp.pos⟩
 
 instance decidable_eq : decidable_eq (zmodp p hp) := fin.decidable_eq _
 
+instance X (h : prime 2) : subsingleton (units (zmodp 2 h)) :=
+zmod.subsingleton
+
 instance : has_repr (zmodp p hp) := fin.has_repr _
 
 @[simp] lemma card_zmodp : fintype.card (zmodp p hp) = p :=

src/data/zmod/quadratic_reciprocity.lean

@@ -42,7 +42,7 @@ by rw [← units.mk0_val ha, ← @units.coe_one (zmodp p hp), ← units.coe_pow,
 lemma euler_criterion_units {x : units (zmodp p hp)} :
   (∃ y : units (zmodp p hp), y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
 hp.eq_two_or_odd.elim
-  (λ h, by resetI; subst h; revert x; exact dec_trivial)
+  (λ h, by resetI; subst h; exact iff_of_true ⟨1, subsingleton.elim _ _⟩ (subsingleton.elim _ _))
   (λ hp1, let ⟨g, hg⟩ := is_cyclic.exists_generator (units (zmodp p hp)) in
     let ⟨n, hn⟩ := show x ∈ powers g, from (powers_eq_gpowers g).symm ▸ hg x in
     ⟨λ ⟨y, hy⟩, by rw [← hy, ← pow_mul, two_mul_odd_div_two hp1,

src/field_theory/finite.lean

@@ -87,10 +87,6 @@ end polynomial
 section
 variables [field α] [fintype α]
 
-instance [decidable_eq α] : fintype (units α) :=
-by haveI := set_fintype {a : α | a ≠ 0}; exact
-fintype.of_equiv _ (equiv.units_equiv_ne_zero α).symm
-
 lemma card_units [decidable_eq α] : fintype.card (units α) = fintype.card α - 1 :=
 begin
   rw [eq_comm, nat.sub_eq_iff_eq_add (fintype.card_pos_iff.2 ⟨(0 : α)⟩)],
@@ -159,3 +155,24 @@ let ⟨a, b, hab⟩ := zmodp.sum_two_squares (show nat.prime n,
 end⟩
 
 end char_p
+
+open_locale nat
+open zmod
+
+/-- The Fermat-Euler totient theorem. `nat.modeq.pow_totient` is an alternative statement
+  of the same theorem. -/
+@[simp] lemma zmod.pow_totient {n : ℕ+} (x : units (zmod n)) : x ^ φ n = 1 :=
+by rw [← card_units_eq_totient, pow_card_eq_one]
+
+/-- The Fermat-Euler totient theorem. `zmod.pow_totient` is an alternative statement
+  of the same theorem. -/
+lemma nat.modeq.pow_totient {x n : ℕ} (h : nat.coprime x n) : x ^ φ n ≡ 1 [MOD n] :=
+begin
+  rcases nat.eq_zero_or_pos n with rfl | h₁, {simp},
+  let n' : ℕ+ := ⟨n, h₁⟩,
+  let x' : units (zmod n') := zmod.unit_of_coprime _ h,
+  have := zmod.pow_totient x',
+  apply (zmod.eq_iff_modeq_nat' h₁).1,
+  apply_fun (coe:units (zmod n') → zmod n') at this,
+  simpa [show (x':zmod n') = x, from rfl],
+end