Theorems · Definition · commutative algebra

Algebra.EssFiniteType.finset

(R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [h : Algebra.EssFiniteType R S] → Finset S

Let S be an R-algebra essentially of finite type, this is a choice of a finset s ⊆ S such that S is the localization of R[s].

Defined in

Mathlib.RingTheory.EssentialFiniteness

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.EssFiniteType