adjoin_of_finite — Mathlib

English

If t is a finite set of elements in A, then the subalgebra generated by t over R is finitely generated.

Русский

Если t — конечное множество элементов в A, то подалгебра, порождаемая t над R, конечна по порождению.

LaTeX

$$t.Finite → Algebra.FiniteType\\ R\\ (Subtype fun x => SetLike.instMembership.mem (Algebra.adjoin R t) x)$$

Lean4

theorem adjoin_of_finite {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} (h : Set.Finite t) :
    FiniteType R (Algebra.adjoin R t) := by
  rw [← Subalgebra.fg_iff_finiteType]
  exact ⟨h.toFinset, by simp⟩

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