From 17ea68aaf414358bae185d2b9eb1c966c360e870 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Wed, 25 Aug 2021 09:24:29 +0000 Subject: [PATCH] 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