Theorems · Theorem · commutative algebra

RingHom.finite_of_algHom_finiteType_of_isJacobsonRing

∀ {K : Type u_1} {L : Type u_2} {A : Type u_3} [inst : CommRing K] [inst_1 : Field L] [inst_2 : CommRing A]
  [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] (f : K →+* L) (g : L →+* A), (g.comp f).FiniteType → f.Finite

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 149 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldCommRingIsJacobsonRingIsNoetherianRingNontrivial