finset — Mathlib

English

If S is an R-algebra essentially of finite type, there exists a finite subset σ of S such that S is the localization of R[σ].

Русский

Если S является R-алгеброй, по сути конечного типа, существует конечное подмножество σ ⊆ S такое, что S является локализацией кольца R[σ].

LaTeX

$$$\exists \sigma \subseteq S\ \, (S \text{ локализация от } R[\sigma])$$$

Lean4

/-- 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]`. -/
noncomputable def finset [h : EssFiniteType R S] : Finset S :=
  h.cond.choose

Похожие утверждения