∀ {K : Type u_1} {L : Type u_2} {A : Type u_3} [inst : CommRing K] [inst_1 : DivisionRing L] [inst_2 : CommRing A]
  [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] [inst_6 : Algebra K L] [inst_7 : Algebra K A]
  [Algebra.FiniteType K A] (f : L →ₐ[K] A), Module.Finite K L