counting field embeddings

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

variable (F K L : Type*)
  [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Module.Finite F K]

theorem card_algHom_of_isGalois [IsGalois F K] (h : K →ₐ[F] L) :
    Fintype.card (K →ₐ[F] L) = Fintype.card Gal(K/F) :=
  sorry

[Aaron Liu]

I just spent 30 minutes trying to prove this before finding docs#Normal.algHomEquivAut

[Aaron Liu]

you can just feed it the docs#RingHom.toAlgebra and docs#IsScalarTower.of_algHom

[Aaron Liu]

I think for this lemma you only need K/F to be "relatively normal" in L, is "relatively normal" in mathlib?