Theorems · Inductive type · commutative algebra

Algebra.EssFiniteType

(R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop

An R-algebra is essentially of finite type if it is the localization of an algebra of finite type. See essFiniteType_iff_exists_subalgebra. For field extensions, this is equivalent to being finitely generated as a field. See IntermediateField.fg_top_iff.

Defined in

Mathlib.RingTheory.EssentialFiniteness

Cited by

68 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebra