subalgebra — Mathlib

English

For EssFiniteType R S, the subalgebra of S consisting of elements that lie in the ess finite type subalgebra is itself of finite type over R.

Русский

Пусть R/S имеют существенный конечный тип; подалгебра S, состоящая из элементов essFiniteType-подалгебры, сама по себе является конечного типа над R.

LaTeX

$$$\text{Algebra.FiniteType } R (\text{Subtype }(x \in \text{EssFiniteType.subalgebra } R S))$$$

Lean4

/-- A choice of a subalgebra of finite type in an essentially of finite type algebra, such that
its localization is the whole ring. -/
noncomputable abbrev subalgebra [EssFiniteType R S] : Subalgebra R S :=
  Algebra.adjoin R (finset R S : Set S)

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