instSmall — Mathlib

English

If R and σ are small, then the multivariate polynomial ring MvPolynomial σ R is small.

Русский

Если R и σ малы, то многочлены MvPolynomial σ R также являются малым модулем над R.

LaTeX

$$$\\text{Small}(R) \\wedge \\text{Small}(\\sigma) \\Rightarrow \\text{Small}(\\mathrm{MvPolynomial}(\\sigma,R))$$$

Lean4

instance {σ : Type*} {R : Type*} [CommSemiring R] [Small.{u} R] [Small.{u} σ] : Small.{u} (MvPolynomial σ R) :=
  inferInstanceAs (Small.{u} ((σ →₀ ℕ) →₀ R))

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