instFiniteTypeCarrierObjCommAlgCat

English

If A is a finitely generated commutative R-algebra, then its underlying carrier is a finitely generated R-algebra as an object.

Русский

Если A является конечной порожденной коммутативной R-алгеброй, то её носитель также является алгеброй конечного типа над R.

LaTeX

$$$A.1$ is a finitely generated (over $R$) algebra$$

Lean4

instance (A : FGAlgCat R) : Algebra.FiniteType R A.1 :=
  A.2

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