More elegant proof

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
leanprover-community · Aug 25, 2021 · 17ea68a · 17ea68a
1 parent 2fde8df
commit 17ea68a
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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