feat(field_theory/finite/basic): generalize lemma from field to integ…

…ral domain (#10655)
leanprover-community · Dec 7, 2021 · ae7a88d · ae7a88d
1 parent 9a2c299
commit ae7a88d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/field_theory/finite/basic.lean b/src/field_theory/finite/basic.lean
@@ -97,7 +97,7 @@ calc 2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-
 
 end polynomial
 
-lemma prod_univ_units_id_eq_neg_one [field K] [fintype (units K)] :
+lemma prod_univ_units_id_eq_neg_one [comm_ring K] [is_domain K] [fintype (units K)] :
   (∏ x : units K, x) = (-1 : units K) :=
 begin
   classical,