fg_def — Mathlib

English

A subalgebra S is finitely generated precisely if there exists a finite set t ⊆ A with adjoin_R t = S.

Русский

Подалгебра S конечнопорождается тогда и тогда, когда существует конечный набор t ⊆ A с adjoin_R t = S.

LaTeX

$$$S.FG \\iff \\exists t:\\ Set\\ A, Set.Finite t ∧ Algebra.adjoin R t = S$$$

Lean4

theorem fg_def {S : Subalgebra R A} : S.FG ↔ ∃ t : Set A, Set.Finite t ∧ Algebra.adjoin R t = S :=
  Iff.symm Set.exists_finite_iff_finset

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