polynomial — Mathlib

English

The polynomial ring in finitely many variables over a finitely presented algebra is finitely presented.

Русский

Кольцо многочленов в конечном числе переменных над конечной презентацией алгебры сохраняет конечную презентацию.

LaTeX

$$$[\\text{FinitePresentation } R A] \\Rightarrow \\text{FinitePresentation } R (A[X])$$$

Lean4

/-- `R[X]` is finitely presented as `R`-algebra. -/
instance polynomial [FinitePresentation R A] : FinitePresentation R A[X] :=
  letI := FinitePresentation.mvPolynomial R A Unit
  have := equiv (MvPolynomial.pUnitAlgEquiv.{_, 0} A)
  .trans _ A _

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