polynomial — Mathlib

English

If S is a finite type over R and ι is finite, then the multivariate polynomial ring MvPolynomial_{ι}(S) is of finite type over R.

Русский

Если S конечная по типу над R и индекс ι конечен, то MvPolynomial_{ι}(S) конечна по типу над R.

LaTeX

$$$[Finite ι] \\Rightarrow [Algebra.FiniteType R S] \\Rightarrow [Algebra.FiniteType R (MvPolynomial ι S)]$$$

Lean4

@[deprecated inferInstance (since := "2025-07-12")]
protected theorem polynomial : FiniteType R R[X] :=
  inferInstance

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