mvPolynomial — Mathlib

English

Let ι be a finite index set. Then the multivariate polynomial algebra in indeterminates indexed by ι over a commutative semiring R is a finitely generated R-algebra.

Русский

Пусть ι — конечный индексный набор. Тогда многочленная алгебра в переменных, проиндексированных ι над коммутативным полукольцом R, является конечной по степени порождения R-алгеброй.

LaTeX

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

Lean4

@[deprecated inferInstance (since := "2025-07-12")]
protected theorem mvPolynomial (ι : Type*) [Finite ι] : FiniteType R (MvPolynomial ι R) :=
  inferInstance

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