Theorems · Theorem · commutative algebra

finite_of_algHom_finiteType_of_isJacobsonRing

∀ {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

If K is a Jacobson Noetherian ring, A a nontrivial K-algebra of finite type, then any K-subfield of A is finite over K.

Defined in

Mathlib.RingTheory.Jacobson.Ring

Cited by

1 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingDivisionRingCommRingIsJacobsonRingIsNoetherianRingNontrivialAlgebraAlgebraAlgebra.FiniteType