mvPolynomial — Mathlib

English

If B is finitely presented over A and A is finitely presented over R with IsScalarTower, then B is finitely presented over R.

Русский

Если B имеет конечную презентацию над A, а A — над R, и т. д., тогда B имеет конечную презентацию над R.

LaTeX

$$$[\\text{Algebra } A B] [\\text{IsScalarTower } R A B] [\\text{FinitePresentation } R B] [\\text{FiniteType } R A] : \\; \\text{FinitePresentation } A B$$$

Lean4

/-- The ring of polynomials in finitely many variables is finitely presented. -/
protected instance mvPolynomial [FinitePresentation R A] (ι : Type*) [Finite ι] :
    FinitePresentation R (MvPolynomial ι A) :=
  have := FinitePresentation.mvPolynomial_aux A ι;
  .trans _ A _

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