FG — Mathlib · SciLib

English

The finitely generated-ness of the top subalgebra over R corresponds to the finitely generated-ness of S itself via the top mapping.

Русский

Финитная генерация верхней подалгебры над R эквивалентна генерации самой S.

LaTeX

$$$(\\top : Subalgebra\\ R\\ S).FG \\leftrightarrow S.FG$$$

Lean4

/-- A subalgebra `S` is finitely generated if there exists `t : Finset A` such that
`Algebra.adjoin R t = S`. -/
def FG (S : Subalgebra R A) : Prop :=
  ∃ t : Finset A, Algebra.adjoin R ↑t = S

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