instFreeAlgebraOfFinite — Mathlib

English

Let ι be finite and S be a finitely generated R-algebra. Then the free algebra FreeAlgebra_S(ι) is finitely generated as an R-algebra.

Русский

Пусть ι конечен и S — сконструированная R-алгебра конечного типа. Тогда свободная алгебра FreeAlgebra_S(ι) является конечной по порождению как R-алгебра.

LaTeX

$$$[Finite\\ ι]\\ [FiniteType\\ R\\ S]\\Rightarrow FiniteType\\ R\\ (FreeAlgebra\\ S\\ ι)$$$

Lean4

instance {ι : Type*} [Finite ι] [FiniteType R S] : FiniteType R (FreeAlgebra S ι) := by
  classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..

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