From 41c42fe547a42d578687d582808f7d102a8ecfa5 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 19 Aug 2021 11:00:02 +0000
Subject: [PATCH 01/10] feat(field_theory/intermediate_field): generalize
 `algebra` instances

The `algebra` and `is_scalar_tower` instances for `intermediate_field` are (again) as general as those for `subalgebra`.
---
 src/field_theory/intermediate_field.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
index 65ddce1f7d00d..e575c1287ff71 100644
--- a/src/field_theory/intermediate_field.lean
+++ b/src/field_theory/intermediate_field.lean
@@ -208,10 +208,16 @@ end
 instance algebra : algebra K S :=
 S.to_subalgebra.algebra
 
-instance to_algebra : algebra S L :=
+instance to_algebra {R : Type*} [semiring R] [algebra L R] : algebra S R :=
 S.to_subalgebra.to_algebra
 
-instance : is_scalar_tower K S L :=
+instance is_scalar_tower_bot {R R' : Type*} [comm_semiring R] [semiring R']
+  [algebra L R] [algebra R R'] [algebra L R'] [is_scalar_tower L R R'] :
+  is_scalar_tower S L R' :=
+is_scalar_tower.subalgebra _ _ _ S.to_subalgebra
+
+instance is_scalar_tower_mid {R : Type*} [semiring R] [algebra L R] [algebra K R]
+  [is_scalar_tower K L R] : is_scalar_tower K S R :=
 is_scalar_tower.subalgebra' _ _ _ S.to_subalgebra
 
 variables {L' : Type*} [field L'] [algebra K L']

From 232d8b98fbc344e002bc83156c3d2e48523db2ab Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 19 Aug 2021 11:14:42 +0000
Subject: [PATCH 02/10] Lint fix

---
 src/field_theory/intermediate_field.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
index e575c1287ff71..6412257c82451 100644
--- a/src/field_theory/intermediate_field.lean
+++ b/src/field_theory/intermediate_field.lean
@@ -211,9 +211,8 @@ S.to_subalgebra.algebra
 instance to_algebra {R : Type*} [semiring R] [algebra L R] : algebra S R :=
 S.to_subalgebra.to_algebra
 
-instance is_scalar_tower_bot {R R' : Type*} [comm_semiring R] [semiring R']
-  [algebra L R] [algebra R R'] [algebra L R'] [is_scalar_tower L R R'] :
-  is_scalar_tower S L R' :=
+instance is_scalar_tower_bot {R : Type*} [comm_semiring R] [algebra L R] :
+  is_scalar_tower S L R :=
 is_scalar_tower.subalgebra _ _ _ S.to_subalgebra
 
 instance is_scalar_tower_mid {R : Type*} [semiring R] [algebra L R] [algebra K R]

From af3ffa73f1198087786a84b57dcd0d53037fe989 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Tue, 24 Aug 2021 13:15:58 +0000
Subject: [PATCH 03/10] Fix the timeout by making some unifications fail fast

---
 src/field_theory/polynomial_galois_group.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean
index e1e4775ecccbb..ece57a833990b 100644
--- a/src/field_theory/polynomial_galois_group.lean
+++ b/src/field_theory/polynomial_galois_group.lean
@@ -97,6 +97,14 @@ instance [h : fact (p.splits (algebra_map F E))] : is_scalar_tower F p.splitting
 is_scalar_tower.of_algebra_map_eq
   (λ x, ((is_splitting_field.lift p.splitting_field p h.1).commutes x).symm)
 
+-- The `algebra p.splitting_field E` instance above behaves badly when
+-- `E := p.splitting_field`, since it may result in a unification problem
+-- `is_splitting_field.lift.to_ring_hom.to_algebra =?= algebra.id`,
+-- which takes an extremely long time to resolve, causing timeouts.
+-- Since we don't really care about this definition, marking it as irreducible
+-- causes that unification to error out early.
+attribute [irreducible] gal.algebra
+
 /-- Restrict from a superfield automorphism into a member of `gal p`. -/
 def restrict [fact (p.splits (algebra_map F E))] : (E ≃ₐ[F] E) →* p.gal :=
 alg_equiv.restrict_normal_hom p.splitting_field

From fdad3dd35b1f17b81297fb86ad90c5a29d19cac7 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Tue, 24 Aug 2021 14:34:54 +0000
Subject: [PATCH 04/10] Specialize `intermediate_field.is_scalar_tower_mid`

Use a specialized instance for the common case `is_scalar_tower K S L`, which
was the only instance in the old situation.
---
 src/field_theory/intermediate_field.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
index 6412257c82451..ac1e1187350ee 100644
--- a/src/field_theory/intermediate_field.lean
+++ b/src/field_theory/intermediate_field.lean
@@ -211,7 +211,7 @@ S.to_subalgebra.algebra
 instance to_algebra {R : Type*} [semiring R] [algebra L R] : algebra S R :=
 S.to_subalgebra.to_algebra
 
-instance is_scalar_tower_bot {R : Type*} [comm_semiring R] [algebra L R] :
+instance is_scalar_tower_bot {R : Type*} [semiring R] [algebra L R] :
   is_scalar_tower S L R :=
 is_scalar_tower.subalgebra _ _ _ S.to_subalgebra
 
@@ -219,6 +219,10 @@ instance is_scalar_tower_mid {R : Type*} [semiring R] [algebra L R] [algebra K R
   [is_scalar_tower K L R] : is_scalar_tower K S R :=
 is_scalar_tower.subalgebra' _ _ _ S.to_subalgebra
 
+/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L` -/
+instance is_scalar_tower_mid' : is_scalar_tower K S L :=
+S.is_scalar_tower_mid
+
 variables {L' : Type*} [field L'] [algebra K L']
 
 /-- If `f : L →+* L'` fixes `K`, `S.map f` is the intermediate field between `L'` and `K`

From a32df1c9f8c02b3b82acfc126bb39c6ba96144fd Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Wed, 18 Aug 2021 13:49:11 +0000
Subject: [PATCH 05/10] chore(ring_theory/power_basis): `@[simps]`
 `lift_equiv'`

---
 src/ring_theory/power_basis.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ring_theory/power_basis.lean b/src/ring_theory/power_basis.lean
index b4534d0d39f2d..bcb37d04dcdaf 100644
--- a/src/ring_theory/power_basis.lean
+++ b/src/ring_theory/power_basis.lean
@@ -329,6 +329,7 @@ noncomputable def lift_equiv (pb : power_basis A S) :
 
 /-- `pb.lift_equiv'` states that elements of the root set of the minimal
 polynomial of `pb.gen` correspond to maps sending `pb.gen` to that root. -/
+@[simps {fully_applied := ff}]
 noncomputable def lift_equiv' (pb : power_basis A S) :
   (S →ₐ[A] B) ≃ {y : B // y ∈ ((minpoly A pb.gen).map (algebra_map A B)).roots} :=
 pb.lift_equiv.trans ((equiv.refl _).subtype_equiv (λ x,

From f166b338e0f509e3ab9253802c42da34cc284c93 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Wed, 18 Aug 2021 14:41:49 +0000
Subject: [PATCH 06/10] feat(field_theory): cardinality of `alg_hom`s out of a
 finite separable extension

---
 src/field_theory/adjoin.lean            |  4 +++-
 src/field_theory/primitive_element.lean | 14 ++++++++++++++
 src/field_theory/separable.lean         |  4 ++--
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean
index a7e58649a9011..3f380549821a4 100644
--- a/src/field_theory/adjoin.lean
+++ b/src/field_theory/adjoin.lean
@@ -530,7 +530,9 @@ lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minpoly F α
   (h_splits : (minpoly F α).splits (algebra_map F K)) :
   @fintype.card (F⟮α⟯ →ₐ[F] K) (fintype_of_alg_hom_adjoin_integral F h) =
     (minpoly F α).nat_degree :=
-by { rw alg_hom.card_of_power_basis, all_goals { rwa [adjoin.power_basis_gen, minpoly_gen h] } }
+by rw alg_hom.card_of_power_basis;
+     simp only [adjoin.power_basis_dim, adjoin.power_basis_gen, minpoly_gen h];
+     assumption
 
 end adjoin_integral_element
 
diff --git a/src/field_theory/primitive_element.lean b/src/field_theory/primitive_element.lean
index ade36a55a1300..50efa64d8ae59 100644
--- a/src/field_theory/primitive_element.lean
+++ b/src/field_theory/primitive_element.lean
@@ -5,6 +5,7 @@ Authors: Thomas Browning, Patrick Lutz
 -/
 
 import field_theory.adjoin
+import field_theory.algebraic_closure
 import field_theory.separable
 
 /-!
@@ -194,4 +195,17 @@ let α := (exists_primitive_element F E).some,
 have e : F⟮α⟯ = ⊤ := (exists_primitive_element F E).some_spec,
 pb.map ((intermediate_field.equiv_of_eq e).trans intermediate_field.top_equiv)
 
+/-- If `E / F` is a finite separable extension, then there are finitely many
+embeddings from `E` into `K` that fix `F`, corresponding to the number of
+conjugate roots of the primitive element generating `F`. -/
+instance {K : Type*} [field K] [algebra F K] : fintype (E →ₐ[F] K) :=
+power_basis.alg_hom.fintype (power_basis_of_finite_of_separable F E)
+
 end field
+
+@[simp] lemma alg_hom.card (F E K : Type*) [field F] [field E] [field K] [is_alg_closed K]
+  [algebra F E] [finite_dimensional F E] [is_separable F E] [algebra F K] :
+  fintype.card (E →ₐ[F] K) = finrank F E :=
+(alg_hom.card_of_power_basis (field.power_basis_of_finite_of_separable F E)
+    (is_separable.separable _ _) (is_alg_closed.splits_codomain _)).trans
+  (power_basis.finrank _).symm
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 854db31713776..0bc6f2e9738b9 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -657,12 +657,12 @@ variables [algebra K S] [algebra K L]
 
 lemma alg_hom.card_of_power_basis (pb : power_basis K S) (h_sep : (minpoly K pb.gen).separable)
   (h_splits : (minpoly K pb.gen).splits (algebra_map K L)) :
-  @fintype.card (S →ₐ[K] L) (power_basis.alg_hom.fintype pb) = (minpoly K pb.gen).nat_degree :=
+  @fintype.card (S →ₐ[K] L) (power_basis.alg_hom.fintype pb) = pb.dim :=
 begin
   let s := ((minpoly K pb.gen).map (algebra_map K L)).roots.to_finset,
   have H := λ x, multiset.mem_to_finset,
   rw [fintype.card_congr pb.lift_equiv', fintype.card_of_subtype s H,
-      nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
+      ← pb.nat_degree_minpoly, nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
   exact nodup_roots ((separable_map (algebra_map K L)).mpr h_sep)
 end
 

From 2691f0ba20304018224ccb6fa41c95997e775446 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 19 Aug 2021 10:28:55 +0000
Subject: [PATCH 07/10] Golf/speedup

---
 src/linear_algebra/free_module_pid.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/linear_algebra/free_module_pid.lean b/src/linear_algebra/free_module_pid.lean
index 7c202dddbfc12..de12faf5fe42e 100644
--- a/src/linear_algebra/free_module_pid.lean
+++ b/src/linear_algebra/free_module_pid.lean
@@ -437,9 +437,7 @@ begin
         (show (set.range (λ ψ : M →ₗ[R] R, ψ.submodule_image N)).nonempty,
          from ⟨_, set.mem_range.mpr ⟨0, rfl⟩⟩),
     obtain ⟨ϕ, rfl⟩ := set.mem_range.mp P_eq,
-    use ϕ,
-    intros ψ hψ,
-    exact P_max _ ⟨_, rfl⟩ hψ },
+    exact ⟨ϕ, λ ψ hψ, P_max _ ⟨_, rfl⟩ hψ⟩ },
   let ϕ := this.some,
   have ϕ_max := this.some_spec,
   -- Since `ϕ(N)` is a `R`-submodule of the PID `R`,

From 2fde8df5780d1b264c5d9a315d02cb29398867b6 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 19 Aug 2021 12:07:16 +0000
Subject: [PATCH 08/10] =?UTF-8?q?feat(ring=5Ftheory/trace):=20Tr(x)=20is?=
 =?UTF-8?q?=20the=20sum=20of=20embeddings=20=CF=83=20x=20into=20an=20algeb?=
 =?UTF-8?q?raically=20closed=20field?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/ring_theory/trace.lean | 87 ++++++++++++++++++++++++++++++++++----
 1 file changed, 78 insertions(+), 9 deletions(-)

diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index 4650912c1abe8..76d112666c22c 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -6,9 +6,10 @@ Authors: Anne Baanen
 
 import linear_algebra.bilinear_form
 import linear_algebra.char_poly.coeff
+import linear_algebra.determinant
 import linear_algebra.trace
-import field_theory.adjoin
 import field_theory.algebraic_closure
+import field_theory.primitive_element
 import ring_theory.power_basis
 
 /-!
@@ -232,20 +233,29 @@ end
 
 end intermediate_field.adjoin_simple
 
-lemma trace_eq_sum_roots [finite_dimensional K L]
-  {x : L} (hF : (minpoly K x).splits (algebra_map K F)) :
-  algebra_map K F (algebra.trace K L x) =
-    finrank K⟮x⟯ L • ((minpoly K x).map (algebra_map K _)).roots.sum :=
+open intermediate_field
+
+variables (K)
+
+lemma trace_eq_trace_adjoin [finite_dimensional K L] (x : L) :
+  algebra.trace K L x = finrank K⟮x⟯ L • trace K K⟮x⟯ (adjoin_simple.gen K x) :=
 begin
-  haveI : finite_dimensional K⟮x⟯ L := finite_dimensional.right K _ L,
   rw ← @trace_trace _ _ K K⟮x⟯ _ _ _ _ _ _ _ _ x,
   conv in x { rw ← intermediate_field.adjoin_simple.algebra_map_gen K x },
   rw [trace_algebra_map, ← is_scalar_tower.algebra_map_smul K, (algebra.trace K K⟮x⟯).map_smul,
-      smul_eq_mul, ring_hom.map_mul, ← is_scalar_tower.algebra_map_apply ℕ K _, ← smul_def,
-      intermediate_field.adjoin_simple.trace_gen_eq_sum_roots _ hF],
-  all_goals { apply_instance }
+      smul_eq_mul, algebra.smul_def],
+  apply_instance
 end
 
+variables {K}
+
+lemma trace_eq_sum_roots [finite_dimensional K L]
+  {x : L} (hF : (minpoly K x).splits (algebra_map K F)) :
+  algebra_map K F (algebra.trace K L x) =
+    finrank K⟮x⟯ L • ((minpoly K x).map (algebra_map K _)).roots.sum :=
+by rw [trace_eq_trace_adjoin K x, algebra.smul_def, ring_hom.map_mul, ← algebra.smul_def,
+    intermediate_field.adjoin_simple.trace_gen_eq_sum_roots _ hF, is_scalar_tower.algebra_map_smul]
+
 end eq_sum_roots
 
 variables {F : Type*} [field F]
@@ -268,3 +278,62 @@ begin
   { apply is_alg_closed.splits_codomain },
   { apply_instance }
 end
+
+section eq_sum_embeddings
+
+variables [algebra K F] [is_scalar_tower K L F]
+
+open algebra intermediate_field
+
+lemma trace_eq_sum_embeddings_gen (E : Type*) [field E] [algebra K E]
+  (pb : power_basis K L)
+  (hE : (minpoly K pb.gen).splits (algebra_map K E)) (hfx : (minpoly K pb.gen).separable) :
+  algebra_map K E (algebra.trace K L pb.gen) =
+    (@@finset.univ (power_basis.alg_hom.fintype pb)).sum (λ σ, σ pb.gen) :=
+begin
+  letI := classical.dec_eq E,
+  rw [pb.trace_gen_eq_sum_roots hE, fintype.sum_equiv pb.lift_equiv', finset.sum_mem_multiset,
+      finset.sum_eq_multiset_sum, multiset.to_finset_val,
+      multiset.erase_dup_eq_self.mpr (nodup_roots ((separable_map _).mpr hfx)), multiset.map_id],
+  { intro x, refl },
+  { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
+end
+
+variables (F)
+lemma sum_embeddings_eq_finrank_mul
+  (E : Type*) [field E] [is_alg_closed E]
+  [algebra K E]  [finite_dimensional K F] [is_separable K F]
+  (pb : power_basis K L) :
+  ∑ σ : F →ₐ[K] E, σ (algebra_map L F pb.gen) =
+    finrank L F • (@@finset.univ (power_basis.alg_hom.fintype pb)).sum
+      (λ σ : L →ₐ[K] E, σ pb.gen) :=
+begin
+  haveI : finite_dimensional L F := finite_dimensional.right K L F,
+  haveI : is_separable L F := is_separable_tower_top_of_is_separable K L F,
+  letI : fintype (L →ₐ[K] E) := power_basis.alg_hom.fintype pb,
+  letI : ∀ (f : L →ₐ[K] E), fintype (@@alg_hom L F E _ _ _ _ f.to_ring_hom.to_algebra) :=
+    _, -- will be solved by unification
+  rw [fintype.sum_equiv alg_hom_equiv_sigma (λ (σ : F →ₐ[K] E), _) (λ σ, σ.1 pb.gen),
+      ← finset.univ_sigma_univ, finset.sum_sigma, ← finset.sum_nsmul],
+  refine finset.sum_congr rfl (λ σ _, _),
+  { letI : algebra L E := σ.to_ring_hom.to_algebra,
+    simp only [finset.sum_const, finset.card_univ],
+    rw alg_hom.card L F E },
+  { intros σ,
+    simp only [alg_hom_equiv_sigma, equiv.coe_fn_mk, alg_hom.restrict_domain, alg_hom.comp_apply,
+         is_scalar_tower.coe_to_alg_hom'] }
+end
+
+lemma trace_eq_sum_embeddings [is_alg_closed F] [finite_dimensional K L] [is_separable K L]
+  {x : L} (hx : is_integral K x) :
+  algebra_map K F (algebra.trace K L x) = ∑ σ : L →ₐ[K] F, σ x :=
+begin
+  rw [trace_eq_trace_adjoin K x, algebra.smul_def, ring_hom.map_mul, ← adjoin.power_basis_gen hx,
+      trace_eq_sum_embeddings_gen F (adjoin.power_basis hx) (is_alg_closed.splits_codomain _),
+      ← algebra.smul_def, algebra_map_smul],
+  { exact (sum_embeddings_eq_finrank_mul L F (adjoin.power_basis hx)).symm },
+  { haveI := is_separable_tower_bot_of_is_separable K K⟮x⟯ L,
+    exact is_separable.separable K _ }
+end
+
+end eq_sum_embeddings

From 17ea68aaf414358bae185d2b9eb1c966c360e870 Mon Sep 17 00:00:00 2001
From: Anne Baanen <Vierkantor@users.noreply.github.com>
Date: Wed, 25 Aug 2021 09:24:29 +0000
Subject: [PATCH 09/10] More elegant proof

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
---
 src/field_theory/adjoin.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean
index 3f380549821a4..61f58be053015 100644
--- a/src/field_theory/adjoin.lean
+++ b/src/field_theory/adjoin.lean
@@ -530,9 +530,10 @@ lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minpoly F α
   (h_splits : (minpoly F α).splits (algebra_map F K)) :
   @fintype.card (F⟮α⟯ →ₐ[F] K) (fintype_of_alg_hom_adjoin_integral F h) =
     (minpoly F α).nat_degree :=
-by rw alg_hom.card_of_power_basis;
-     simp only [adjoin.power_basis_dim, adjoin.power_basis_gen, minpoly_gen h];
-     assumption
+begin
+  rw alg_hom.card_of_power_basis;
+    simp only [adjoin.power_basis_dim, adjoin.power_basis_gen, minpoly_gen h, h_sep, h_splits],
+end
 
 end adjoin_integral_element
 

From 91372ec8fd9533ab434ff815a830573dfc2d5339 Mon Sep 17 00:00:00 2001
From: Anne Baanen <t.baanen@vu.nl>
Date: Thu, 26 Aug 2021 12:22:46 +0200
Subject: [PATCH 10/10] Lint fix, by rearranging variables

---
 src/ring_theory/trace.lean | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index 76d112666c22c..9be2b71913f6c 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -285,7 +285,9 @@ variables [algebra K F] [is_scalar_tower K L F]
 
 open algebra intermediate_field
 
-lemma trace_eq_sum_embeddings_gen (E : Type*) [field E] [algebra K E]
+variables (F) (E : Type*) [field E] [algebra K E]
+
+lemma trace_eq_sum_embeddings_gen
   (pb : power_basis K L)
   (hE : (minpoly K pb.gen).splits (algebra_map K E)) (hfx : (minpoly K pb.gen).separable) :
   algebra_map K E (algebra.trace K L pb.gen) =
@@ -299,10 +301,9 @@ begin
   { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
 end
 
-variables (F)
-lemma sum_embeddings_eq_finrank_mul
-  (E : Type*) [field E] [is_alg_closed E]
-  [algebra K E]  [finite_dimensional K F] [is_separable K F]
+variables [is_alg_closed E]
+
+lemma sum_embeddings_eq_finrank_mul [finite_dimensional K F] [is_separable K F]
   (pb : power_basis K L) :
   ∑ σ : F →ₐ[K] E, σ (algebra_map L F pb.gen) =
     finrank L F • (@@finset.univ (power_basis.alg_hom.fintype pb)).sum
@@ -324,14 +325,14 @@ begin
          is_scalar_tower.coe_to_alg_hom'] }
 end
 
-lemma trace_eq_sum_embeddings [is_alg_closed F] [finite_dimensional K L] [is_separable K L]
+lemma trace_eq_sum_embeddings [finite_dimensional K L] [is_separable K L]
   {x : L} (hx : is_integral K x) :
-  algebra_map K F (algebra.trace K L x) = ∑ σ : L →ₐ[K] F, σ x :=
+  algebra_map K E (algebra.trace K L x) = ∑ σ : L →ₐ[K] E, σ x :=
 begin
   rw [trace_eq_trace_adjoin K x, algebra.smul_def, ring_hom.map_mul, ← adjoin.power_basis_gen hx,
-      trace_eq_sum_embeddings_gen F (adjoin.power_basis hx) (is_alg_closed.splits_codomain _),
+      trace_eq_sum_embeddings_gen E (adjoin.power_basis hx) (is_alg_closed.splits_codomain _),
       ← algebra.smul_def, algebra_map_smul],
-  { exact (sum_embeddings_eq_finrank_mul L F (adjoin.power_basis hx)).symm },
+  { exact (sum_embeddings_eq_finrank_mul L E (adjoin.power_basis hx)).symm },
   { haveI := is_separable_tower_bot_of_is_separable K K⟮x⟯ L,
     exact is_separable.separable K _ }
 end