chore(ring_theory/integral_domain): dedup, tidy (#13180)

leanprover-community · Apr 5, 2022 · 91dd3b1 · 91dd3b1
1 parent da132ec
commit 91dd3b1
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 8 deletions.
diff --git a/src/field_theory/finite/basic.lean b/src/field_theory/finite/basic.lean
@@ -20,7 +20,7 @@ and `q` is notation for the cardinality of `K`.
 
 See `ring_theory.integral_domain` for the fact that the unit group of a finite field is a
 cyclic group, as well as the fact that every finite integral domain is a field
-(`field_of_is_domain`).
+(`fintype.field_of_domain`).
 
 ## Main results
 

diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
@@ -16,9 +16,12 @@ Assorted theorems about integral domains.
 
 ## Main theorems
 
-* `is_cyclic_of_subgroup_is_domain` : A finite subgroup of the units of an integral domain
-                                            is cyclic.
-* `field_of_is_domain`              : A finite integral domain is a field.
+* `is_cyclic_of_subgroup_is_domain`: A finite subgroup of the units of an integral domain is cyclic.
+* `fintype.field_of_domain`: A finite integral domain is a field.
+
+## TODO
+
+Prove Wedderburn's little theorem, which shows that all finite division rings are actually fields.
 
 ## Tags
 
@@ -111,10 +114,6 @@ To support `ℤˣ` and other infinite monoids with finite groups of units, this
 instance [fintype Rˣ] : is_cyclic Rˣ :=
 is_cyclic_of_subgroup_is_domain (units.coe_hom R) $ units.ext
 
-/-- Every finite integral domain is a field. -/
-def field_of_is_domain [decidable_eq R] [fintype R] : field R :=
-{ ..fintype.division_ring_of_is_domain R, ..‹comm_ring R› }
-
 section
 
 variables (S : subgroup Rˣ) [fintype S]