(F : Type u_3) →
  (E : Type u_4) →
    (K : Type u_5) →
      [inst : Field F] →
        [inst_1 : Ring E] →
          [inst_2 : CommRing K] →
            [IsDomain K] →
              [inst_4 : Algebra F E] → [inst_5 : Algebra F K] → [FiniteDimensional F E] → Fintype (E →ₐ[F] K)