From 12a85fac627bea918960da036049d611b1a3ee43 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Wed, 31 May 2023 00:27:53 +0000
Subject: [PATCH] chore(field_theory/finite/basic): move a lemma (#19130)

Moving one instance we can erase `field_theory.splitting_field` from the imports of `field_theory.finite.basic)`.
---
 src/field_theory/finite/basic.lean        | 20 --------------------
 src/field_theory/finite/galois_field.lean | 20 +++++++++++++++++++-
 2 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/src/field_theory/finite/basic.lean b/src/field_theory/finite/basic.lean
index 1df22603ad038..75b448e404c72 100644
--- a/src/field_theory/finite/basic.lean
+++ b/src/field_theory/finite/basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Joey van Langen, Casper Putz
 -/
 import field_theory.separable
-import field_theory.splitting_field
 import ring_theory.integral_domain
 import tactic.apply_fun
 
@@ -219,7 +218,6 @@ begin
     ... = 0 : by { rw [sum_pow_units K i, if_neg], exact hiq, }
 end
 
-section is_splitting_field
 open polynomial
 
 section
@@ -268,24 +266,6 @@ begin
       zero_sub] },
   end
 
-instance (F : Type*) [field F] [algebra F K] : is_splitting_field F K (X^q - X) :=
-{ splits :=
-  begin
-    have h : (X^q - X : K[X]).nat_degree = q :=
-      X_pow_card_sub_X_nat_degree_eq K fintype.one_lt_card,
-    rw [←splits_id_iff_splits, splits_iff_card_roots, polynomial.map_sub, polynomial.map_pow,
-      map_X, h, roots_X_pow_card_sub_X K, ←finset.card_def, finset.card_univ],
-  end,
-  adjoin_roots :=
-  begin
-    classical,
-    transitivity algebra.adjoin F ((roots (X^q - X : K[X])).to_finset : set K),
-    { simp only [polynomial.map_pow, map_X, polynomial.map_sub], },
-    { rw [roots_X_pow_card_sub_X, val_to_finset, coe_univ, algebra.adjoin_univ], }
-  end }
-
-end is_splitting_field
-
 variables {K}
 
 theorem frobenius_pow {p : ℕ} [fact p.prime] [char_p K p] {n : ℕ} (hcard : q = p^n) :
diff --git a/src/field_theory/finite/galois_field.lean b/src/field_theory/finite/galois_field.lean
index ac9250227e85c..9165891e346a9 100644
--- a/src/field_theory/finite/galois_field.lean
+++ b/src/field_theory/finite/galois_field.lean
@@ -8,6 +8,7 @@ import algebra.char_p.algebra
 import data.zmod.algebra
 import field_theory.finite.basic
 import field_theory.galois
+import field_theory.splitting_field
 
 /-!
 # Galois fields
@@ -30,9 +31,26 @@ It is a finite field with `p ^ n` elements.
 
 noncomputable theory
 
-open polynomial
+open polynomial finset
 open_locale polynomial
 
+instance finite_field.has_sub.sub.polynomial.is_splitting_field (K F : Type*) [field K] [fintype K]
+  [field F] [algebra F K] : is_splitting_field F K (X ^ (fintype.card K) - X) :=
+{ splits :=
+  begin
+    have h : (X ^ (fintype.card K) - X : K[X]).nat_degree = fintype.card K :=
+      finite_field.X_pow_card_sub_X_nat_degree_eq K fintype.one_lt_card,
+    rw [←splits_id_iff_splits, splits_iff_card_roots, polynomial.map_sub, polynomial.map_pow,
+      map_X, h, finite_field.roots_X_pow_card_sub_X K, ←finset.card_def, finset.card_univ],
+  end,
+  adjoin_roots :=
+  begin
+    classical,
+    transitivity algebra.adjoin F ((roots (X ^ (fintype.card K) - X : K[X])).to_finset : set K),
+    { simp only [polynomial.map_pow, map_X, polynomial.map_sub], },
+    { rw [finite_field.roots_X_pow_card_sub_X, val_to_finset, coe_univ, algebra.adjoin_univ], }
+  end }
+
 lemma galois_poly_separable {K : Type*} [field K] (p q : ℕ) [char_p K p] (h : p ∣ q) :
   separable (X ^ q - X : K[X]) :=
 begin