chore(data/fintype/basic): make units.fintype computable (#9846)

This also:
* renames `equiv.units_equiv_ne_zero` to `units_equiv_ne_zero`, and resolves the TODO comment about generalization
* renames and generalizes `finite_field.card_units` to `fintype.card_units`, and proves it right next to the fintype instance
* generalizes some typeclass assumptions in `finite_field.basic` as the linter already required me to tweak them

src/data/equiv/ring.lean

@@ -435,22 +435,3 @@ protected lemma is_domain
   exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }
 
 end ring_equiv
-
-namespace equiv
-
-variables (K : Type*) [division_ring K]
-
-/-- In a division ring `K`, the unit group `units K`
-is equivalent to the subtype of nonzero elements. -/
--- TODO: this might already exist elsewhere for `group_with_zero`
--- deduplicate or generalize
-def units_equiv_ne_zero : units K ≃ {a : K | a ≠ 0} :=
-⟨λ a, ⟨a.1, a.ne_zero⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩
-
-variable {K}
-
-@[simp]
-lemma coe_units_equiv_ne_zero (a : units K) :
-  ((units_equiv_ne_zero K a) : K) = a := rfl
-
-end equiv

src/data/fintype/basic.lean

@@ -711,19 +711,13 @@ by rw [subsingleton.elim f (@unique.fintype α _)]; refl
 @[simp] lemma univ_is_empty {α : Type*} [is_empty α] [fintype α] : @finset.univ α _ = ∅ :=
 finset.ext is_empty_elim
 
-@[simp] lemma fintype.card_subtype_eq (y : α)  :
+@[simp] lemma fintype.card_subtype_eq (y : α) [fintype {x // x = y}] :
   fintype.card {x // x = y} = 1 :=
-begin
-  convert fintype.card_unique,
-  exact unique.subtype_eq _
-end
+fintype.card_unique
 
-@[simp] lemma fintype.card_subtype_eq' (y : α) :
+@[simp] lemma fintype.card_subtype_eq' (y : α) [fintype {x // y = x}] :
   fintype.card {x // y = x} = 1 :=
-begin
-  convert fintype.card_unique,
-  exact unique.subtype_eq' _
-end
+fintype.card_unique
 
 @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
 
@@ -760,9 +754,6 @@ 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
 
 instance {α : Type*} [fintype α] : fintype (option α) :=
@@ -1067,6 +1058,39 @@ lemma set_fintype_card_le_univ {α : Type*} [fintype α] (s : set α) [fintype 
   fintype.card ↥s ≤ fintype.card α :=
 fintype.card_le_of_embedding (function.embedding.subtype s)
 
+section
+variables (α)
+
+/-- The `units α` type is equivalent to a subtype of `α × α`. -/
+@[simps]
+def _root_.units_equiv_prod_subtype [monoid α] :
+  units α ≃ {p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1} :=
+{ to_fun := λ u, ⟨(u, ↑u⁻¹), u.val_inv, u.inv_val⟩,
+  inv_fun := λ p, units.mk (p : α × α).1 (p : α × α).2 p.prop.1 p.prop.2,
+  left_inv := λ u, units.ext rfl,
+  right_inv := λ p, subtype.ext $ prod.ext rfl rfl}
+
+/-- In a `group_with_zero` `α`, the unit group `units α` is equivalent to the subtype of nonzero
+elements. -/
+@[simps]
+def _root_.units_equiv_ne_zero [group_with_zero α] : units α ≃ {a : α // a ≠ 0} :=
+⟨λ a, ⟨a, a.ne_zero⟩, λ a, units.mk0 _ a.prop, λ _, units.ext rfl, λ _, subtype.ext rfl⟩
+
+end
+
+instance [monoid α] [fintype α] [decidable_eq α] : fintype (units α) :=
+fintype.of_equiv _ (units_equiv_prod_subtype α).symm
+
+lemma fintype.card_units [group_with_zero α] [fintype α] [fintype (units α)] :
+  fintype.card (units α) = fintype.card α - 1 :=
+begin
+  classical,
+  rw [eq_comm, nat.sub_eq_iff_eq_add (fintype.card_pos_iff.2 ⟨(0 : α)⟩),
+    fintype.card_congr (units_equiv_ne_zero α)],
+  have := fintype.card_congr (equiv.sum_compl (= (0 : α))).symm,
+  rwa [fintype.card_sum, add_comm, fintype.card_subtype_eq] at this,
+end
+
 namespace function.embedding
 
 /-- An embedding from a `fintype` to itself can be promoted to an equivalence. -/

src/field_theory/chevalley_warning.lean

@@ -99,7 +99,7 @@ theorem char_dvd_card_solutions_family (p : ℕ) [char_p K p]
   (h : (∑ i in s, (f i).total_degree) < fintype.card σ) :
   p ∣ fintype.card {x : σ → K // ∀ i ∈ s, eval x (f i) = 0} :=
 begin
-  have hq : 0 < q - 1, { rw [← card_units, fintype.card_pos_iff], exact ⟨1⟩ },
+  have hq : 0 < q - 1, { rw [← fintype.card_units, fintype.card_pos_iff], exact ⟨1⟩ },
   let S : finset (σ → K) := { x ∈ univ | ∀ i ∈ s, eval x (f i) = 0 },
   have hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → eval x (f i) = 0,
   { intros x, simp only [S, true_and, sep_def, mem_filter, mem_univ], },

src/field_theory/finite/basic.lean

@@ -24,7 +24,7 @@ cyclic group, as well as the fact that every finite integral domain is a field
 
 ## Main results
 
-1. `card_units`: The unit group of a finite field is has cardinality `q - 1`.
+1. `fintype.card_units`: The unit group of a finite field is has cardinality `q - 1`.
 2. `sum_pow_units`: The sum of `x^i`, where `x` ranges over the units of `K`, is
    - `q-1` if `q-1 ∣ i`
    - `0`   otherwise
@@ -36,10 +36,15 @@ cyclic group, as well as the fact that every finite integral domain is a field
 Throughout most of this file, `K` denotes a finite field
 and `q` is notation for the cardinality of `K`.
 
+## Implementation notes
+
+While `fintype (units K)` can be inferred from `fintype K` in the presence of `decidable_eq K`,
+in this file we take the `fintype (units K)` argument directly to reduce the chance of typeclass
+diamonds, as `fintype` carries data.
+
 -/
 
-variables {K : Type*} [field K] [fintype K]
-variables {R : Type*} [comm_ring R] [is_domain R]
+variables {K : Type*} {R : Type*}
 local notation `q` := fintype.card K
 
 open_locale big_operators
@@ -49,6 +54,8 @@ open finset function
 
 section polynomial
 
+variables [comm_ring R] [is_domain R]
+
 open polynomial
 
 /-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
@@ -90,19 +97,7 @@ calc 2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-
 
 end polynomial
 
-lemma card_units : fintype.card (units K) = fintype.card K - 1 :=
-begin
-  classical,
-  rw [eq_comm, nat.sub_eq_iff_eq_add (fintype.card_pos_iff.2 ⟨(0 : K)⟩)],
-  haveI := set_fintype {a : K | a ≠ 0},
-  haveI := set_fintype (@set.univ K),
-  rw [fintype.card_congr (equiv.units_equiv_ne_zero _),
-    ← @set.card_insert _ _ {a : K | a ≠ 0} _ (not_not.2 (eq.refl (0 : K)))
-    (set.fintype_insert _ _), fintype.card_congr (equiv.set.univ K).symm],
-  congr; simp [set.ext_iff, classical.em]
-end
-
-lemma prod_univ_units_id_eq_neg_one :
+lemma prod_univ_units_id_eq_neg_one [field K] [fintype (units K)] :
   (∏ x : units K, x) = (-1 : units K) :=
 begin
   classical,
@@ -115,10 +110,13 @@ begin
       this, mul_one]
 end
 
+section
+variables [group_with_zero K] [fintype K]
+
 lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1 :=
 calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : units K) :
     by rw [units.coe_pow, units.coe_mk0]
-  ... = 1 : by { classical, rw [← card_units, pow_card_eq_one], refl }
+  ... = 1 : by { classical, rw [← fintype.card_units, pow_card_eq_one], refl }
 
 lemma pow_card (a : K) : a ^ q = a :=
 begin
@@ -135,7 +133,9 @@ begin
   { simp [pow_succ, pow_mul, ih, pow_card], },
 end
 
-variable (K)
+end
+
+variables (K) [field K] [fintype K]
 
 theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=
 begin
@@ -167,9 +167,9 @@ end
 lemma forall_pow_eq_one_iff (i : ℕ) :
   (∀ x : units K, x ^ i = 1) ↔ q - 1 ∣ i :=
 begin
-  obtain ⟨x, hx⟩ := is_cyclic.exists_generator (units K),
   classical,
-  rw [← card_units, ← order_of_eq_card_of_forall_mem_gpowers hx, order_of_dvd_iff_pow_eq_one],
+  obtain ⟨x, hx⟩ := is_cyclic.exists_generator (units K),
+  rw [←fintype.card_units, ←order_of_eq_card_of_forall_mem_gpowers hx, order_of_dvd_iff_pow_eq_one],
   split,
   { intro h, apply h },
   { intros h y,
@@ -180,7 +180,7 @@ end
 
 /-- The sum of `x ^ i` as `x` ranges over the units of a finite field of cardinality `q`
 is equal to `0` unless `(q - 1) ∣ i`, in which case the sum is `q - 1`. -/
-lemma sum_pow_units (i : ℕ) :
+lemma sum_pow_units [fintype (units K)] (i : ℕ) :
   ∑ x : units K, (x ^ i : K) = if (q - 1) ∣ i then -1 else 0 :=
 begin
   let φ : units K →* K :=
@@ -193,7 +193,7 @@ begin
   suffices : (q - 1) ∣ i ↔ φ = 1,
   { simp only [this],
     split_ifs with h h, swap, refl,
-    rw [card_units, nat.cast_sub, cast_card_eq_zero, nat.cast_one, zero_sub],
+    rw [fintype.card_units, nat.cast_sub, cast_card_eq_zero, nat.cast_one, zero_sub],
     show 1 ≤ q, from fintype.card_pos_iff.mpr ⟨0⟩ },
   rw [← forall_pow_eq_one_iff, monoid_hom.ext_iff],
   apply forall_congr, intro x,
@@ -371,7 +371,7 @@ end
 
 section
 
-variables {V : Type*} [add_comm_group V] [module K V]
+variables {V : Type*} [fintype K] [division_ring K] [add_comm_group V] [module K V]
 
 -- should this go in a namespace?
 -- finite_dimensional would be natural,
@@ -404,7 +404,7 @@ end
 by { ext a, rw [frobenius_def, zmod.pow_card, ring_hom.id_apply] }
 
 @[simp] lemma card_units (p : ℕ) [fact p.prime] : fintype.card (units (zmod p)) = p - 1 :=
-by rw [card_units, card]
+by rw [fintype.card_units, card]
 
 /-- **Fermat's Little Theorem**: for every unit `a` of `zmod p`, we have `a ^ (p - 1) = 1`. -/
 theorem units_pow_card_sub_one_eq_one (p : ℕ) [fact p.prime] (a : units (zmod p)) :

src/field_theory/finite/polynomial.lean

@@ -61,7 +61,7 @@ lemma eval_indicator_apply_eq_one (a : σ → K) :
   eval a (indicator a) = 1 :=
 have 0 < fintype.card K - 1,
 begin
-  rw [← finite_field.card_units, fintype.card_pos_iff],
+  rw [← fintype.card_units, fintype.card_pos_iff],
   exact ⟨1⟩
 end,
 by { simp only [indicator, (eval a).map_prod, ring_hom.map_sub,

src/ring_theory/integral_domain.lean

@@ -80,8 +80,11 @@ begin
   convert (le_trans (card_nth_roots_subgroup_units f hf hn 1) (card_nth_roots n (f 1)))
 end
 
-/-- The unit group of a finite integral domain is cyclic. -/
-instance [fintype R] : is_cyclic (units R) :=
+/-- The unit group of a finite integral domain is cyclic.
+
+To support `units ℤ` and other infinite monoids with finite groups of units, this requires only
+`fintype (units R)` rather than deducing it from `fintype R`. -/
+instance [fintype (units R)] : is_cyclic (units R) :=
 is_cyclic_of_subgroup_is_domain (units.coe_hom R) $ units.ext
 
 /-- Every finite integral domain is a field. -/